src/Pure/Isar/isar_syn.ML
changeset 58825 950dc7446454
parent 58784 2373b4c61111
child 58947 8e0a7eaffe47
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 01 21:57:08 2014 -0700
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 02 08:03:48 2014 +0200
     1.3 @@ -423,7 +423,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command @{command_spec "context"} "begin local theory context"
     1.6      ((Parse.position Parse.xname >> (fn name =>
     1.7 -        Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
     1.8 +        Toplevel.begin_local_theory true (Named_Target.begin name)) ||
     1.9        Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
    1.10          >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
    1.11        --| Parse.begin);