src/Pure/Isar/specification.ML
changeset 28941 128459bd72d2
parent 28880 f6a547c5dbbf
child 28965 1de908189869
--- a/src/Pure/Isar/specification.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -190,7 +190,7 @@
             val y = Name.name_of b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
-                Position.str_of (Name.pos_of b));
+                Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
         (var, ((Name.map_name (suffix "_raw") name, []), rhs));
@@ -223,7 +223,7 @@
             val y = Name.name_of b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
-                Position.str_of (Name.pos_of b));
+                Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val lthy' = lthy
       |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
@@ -348,7 +348,7 @@
         lthy
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
-          if Name.is_nothing name andalso null atts then
+          if Binding.is_nothing name andalso null atts then
             (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
           else
             let