Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
print fixed names as plain strings;
authorwenzelm
Tue, 23 Oct 2001 22:59:14 +0200
changeset 11915 df030220a2a8
parent 11914 bca734def300
child 11916 82139d3dcdd7
print fixed names as plain strings;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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 ::
isabelle