src/Pure/Isar/element.ML
changeset 28862 53f13f763d4f
parent 28850 6882e110c29a
child 28888 9d19554bc2a0
--- a/src/Pure/Isar/element.ML	Thu Nov 20 14:55:25 2008 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 20 14:55:28 2008 +0100
@@ -138,7 +138,7 @@
 
 fun params_of (Fixes fixes) = fixes |> map
     (fn (x, SOME T, _) => (Name.name_of x, T)
-      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.name_of x), []))
+      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.display x), []))
   | params_of _ = [];
 
 fun prems_of (Assumes asms) = maps (map fst o snd) asms
@@ -161,9 +161,9 @@
       Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
 
-fun pretty_name_atts ctxt (binding, atts) sep =
+fun pretty_name_atts ctxt (b, atts) sep =
   let
-    val name = Name.output binding;
+    val name = Name.display b;
   in if name = "" andalso null atts then []
     else [Pretty.block
       (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
@@ -394,9 +394,9 @@
   | (SOME (x', NONE), _) => (x', NoSyn)
   | (SOME (x', SOME mx'), _) => (x', mx'));
 
-fun rename_var ren (binding, mx) =
+fun rename_var ren (b, mx) =
   let
-    val x = Name.name_of binding;
+    val x = Name.name_of b;
     val (x', mx') = rename_var_name ren (x, mx);
   in (Name.binding x', mx') end;