src/Pure/Isar/isar_syn.ML
changeset 38348 cf7b2121ad9d
parent 38342 09d4a04d5c2e
child 38350 480b2de9927c
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:31:40 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:31:43 2010 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4    Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
     1.5     (Parse.multi_arity --| Parse.begin
     1.6       >> (fn arities => Toplevel.print o
     1.7 -         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
     1.8 +         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal