diff -r 7e839627b9e7 -r 6b2ba4666336 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 19 13:26:19 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 19 13:28:55 2009 +0100
@@ -161,7 +161,7 @@
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
-    val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -171,7 +171,7 @@
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
         fold_map Thm.add_axiom
           (map (apfst (fn a => Binding.map_name (K a) b))
-            (PureThy.name_multi (Binding.name_of b) (map subst props)))
+            (PureThy.name_multi (Name.of_binding b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
 
     (*facts*)
@@ -198,7 +198,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Binding.name_of b;
+            val y = Name.of_binding b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -234,7 +234,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Binding.name_of b;
+            val y = Name.of_binding b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -292,10 +292,10 @@
   | 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 Binding.name_of b);
+          if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -305,7 +305,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Binding.name_of bs;
+            val xs = map Name.of_binding bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props