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);