src/Pure/Isar/isar_syn.ML
changeset 33553 35f2b30593a8
parent 33515 d066e8369a33
child 33671 4b0f2599ed48
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 10 15:33:35 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 10 16:04:57 2009 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4  val _ =
     1.5    OuterSyntax.command "context" "enter local theory context" K.thy_decl
     1.6      (P.name --| P.begin >> (fn name =>
     1.7 -      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name)));
     1.8 +      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
     1.9  
    1.10  
    1.11  (* locales *)
    1.12 @@ -452,7 +452,7 @@
    1.13    OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
    1.14     (P.multi_arity --| P.begin
    1.15       >> (fn arities => Toplevel.print o
    1.16 -         Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities)));
    1.17 +         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
    1.18  
    1.19  val _ =
    1.20    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.21 @@ -470,7 +470,7 @@
    1.22        Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
    1.23        >> P.triple1) --| P.begin
    1.24     >> (fn operations => Toplevel.print o
    1.25 -         Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
    1.26 +         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
    1.27  
    1.28  
    1.29  (* code generation *)