src/Pure/Isar/isar_syn.ML
changeset 38350 480b2de9927c
parent 38348 cf7b2121ad9d
child 38379 67d71449e85b
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:41:16 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:45:38 2010 +0200
     1.3 @@ -406,7 +406,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
     1.6      (Parse.name --| Parse.begin >> (fn name =>
     1.7 -      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
     1.8 +      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
     1.9  
    1.10  
    1.11  (* locales *)