# HG changeset patch
# User wenzelm
# Date 1091176912 -7200
# Node ID b8a95eadbc140ec4cf21cb2d14876d02756c8851
# Parent  666f89fbb860cf7e50ee4a000983ab6d17a17da2
tuned output;

diff -r 666f89fbb860 -r b8a95eadbc14 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Jul 29 17:45:21 2004 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Jul 30 10:41:52 2004 +0200
@@ -285,9 +285,9 @@
     [Pretty.big_list "simplification rules:" (pretty_thms smps),
       Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
       Pretty.big_list "congruences:" (map pretty_cong cngs),
-      Pretty.strs ("loopers:" :: map #1 loop_tacs),
-      Pretty.strs ("unsafe solvers:" :: map solver_name (#1 solvers)),
-      Pretty.strs ("safe solvers:" :: map solver_name (#2 solvers))]
+      Pretty.strs ("loopers:" :: map (quote o #1) loop_tacs),
+      Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)),
+      Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))]
     |> Pretty.chunks |> Pretty.writeln
   end;