--- a/src/Pure/Isar/isar_syn.ML Tue Jul 01 21:57:08 2014 -0700
+++ b/src/Pure/Isar/isar_syn.ML Wed Jul 02 08:03:48 2014 +0200
@@ -423,7 +423,7 @@
val _ =
Outer_Syntax.command @{command_spec "context"} "begin local theory context"
((Parse.position Parse.xname >> (fn name =>
- Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
+ Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
>> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
--| Parse.begin);