src/Pure/Isar/token.ML

 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
 
 (* wrapped syntax *)
 
-fun syntax_generic scan src context =
-  let
+fun syntax_generic scan src0 context =
+  let
+    val src = map (transfer (Context.theory_of context)) src0;
     val (name, pos) = name_of_src src;
     val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
     fun reported_text () =
       if Context_Position.reports_enabled_generic context then