# HG changeset patch
# User wenzelm
# Date 1003870754 -7200
# Node ID df030220a2a86df6ab63eb4afe6216587c3e4f66
# Parent  bca734def300a0df278028a2cee6c0a7ba858444
print fixed names as plain strings;

diff -r bca734def300 -r df030220a2a8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 23 22:58:15 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 23 22:59:14 2001 +0200
@@ -1037,7 +1037,7 @@
 
     fun prt_case (name, (fixes, (lets, asms))) = Pretty.block (Pretty.fbreaks
       (Pretty.str (name ^ ":") ::
-        prt_sect "fix" [] (prt_term o Free) fixes @
+        prt_sect "fix" [] (Pretty.str o fst) fixes @
         prt_sect "let" [Pretty.str "and"] prt_let
           (mapfilter (fn (xi, Some t) => Some (xi, t) | _ => None) lets) @
         prt_sect "assume" [] (Pretty.quote o prt_term) asms));
@@ -1083,7 +1083,7 @@
 
     (*fixes*)
     fun prt_fix (x, x') = Pretty.block
-      [prt_term (Syntax.free x), Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
+      [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
 
     fun prt_fixes [] = []
       | prt_fixes xs = [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::