src/Pure/Pure.thy
changeset 72453 e4dde7beab39
parent 72434 cc27cf7e51c6
child 72536 589645894305
--- a/src/Pure/Pure.thy	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Pure.thy	Mon Oct 12 07:25:38 2020 +0000
@@ -626,9 +626,10 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
-    ((Parse.name_position >> (Toplevel.begin_main_target true o Named_Target.begin) ||
+    ((Parse.name_position
+        >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
-        >> (fn (incls, elems) => Toplevel.begin_nested_target (#2 o Bundle.context_cmd incls elems)))
+        >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems)))
       --| Parse.begin);
 
 val _ =