src/Pure/Isar/specification.ML

 
     (*axioms*)
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
         fold_map Thm.add_axiom_global
           (map (apfst (fn a => Binding.map_name (K a) b))
-            (Global_Theory.name_multi (Variable.check_name b) (map subst props)))
+            (Global_Theory.name_multi (Binding.name_of b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
       |> Named_Target.theory_init

         val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
       in (([], prems, stmt, NONE), goal_ctxt) end
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
-          if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b);
+          if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
             (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);