src/Pure/Isar/element.ML

 fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
 
 fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
-      (Variable.name (binding (Binding.name x)), typ T)))
+      (Variable.check_name (binding (Binding.name x)), typ T)))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
       ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
       ((binding a, map attrib atts), (term t, map pattern ps))))
    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>

     val ctxt' = Context.proof_map (init elem') ctxt;
   in (map_ctxt_attrib Args.closure elem', ctxt') end;
 
 fun activate raw_elem ctxt =
   let val elem = raw_elem |> map_ctxt
-   {binding = tap Variable.name,
+   {binding = tap Variable.check_name,
     typ = I,
     term = I,
     pattern = I,
     fact = Proof_Context.get_fact ctxt,
     attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}