diff --git a/lib/test/Requalify_Test.thy b/lib/test/Requalify_Test.thy index 2015a1dcf9..ec29c9675c 100644 --- 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