src/Pure/Isar/obtain.ML

     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
-    val xs = map (Variable.name o #1) vars;
+    val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;

     val rule'' = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
   in ((vars', rule''), ctxt') end;
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Variable.name binding;
+    val x = Variable.check_name binding;
     val (T, ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic ctxt vars =
   let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))