[squash] locale requalify inside locale context example

seL4 · Jul 22, 2024 · b1f331a · b1f331a
1 parent b353544
commit b1f331a
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/lib/test/Requalify_Test.thy b/lib/test/Requalify_Test.thy
@@ -72,10 +72,10 @@ requalify_consts (in Requalify_Example2) Requalify_Example1.ex1_const
 requalify_facts (in Requalify_Example2) Requalify_Example1.ex1_const_def
 
 (* this is equivalent to doing the requalifications in the locale context *)
-context Requalify_Example2 begin
-requalify_types (in Requalify_Example2) Requalify_Example1.ex1_type
-requalify_consts (in Requalify_Example2) Requalify_Example1.ex1_const
-requalify_facts (in Requalify_Example2) Requalify_Example1.ex1_const_def
+context Requalify_Example1 begin
+requalify_types (in Requalify_Example2) ex1_type
+requalify_consts (in Requalify_Example2) ex1_const
+requalify_facts (in Requalify_Example2) ex1_const_def
 end
 
 typ Requalify_Example2.ex1_type