src/Pure/Isar/isar_syn.ML
changeset 59890 01aff5aa081d
parent 59064 a8bcb5a446c8
child 59901 840d03805755
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 01 11:55:23 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 01 13:32:32 2015 +0200
@@ -361,7 +361,7 @@
     ((Parse.position Parse.xname >> (fn 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)))
+        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
       --| Parse.begin);