# HG changeset patch
# User wenzelm
# Date 878201978 -3600
# Node ID bd686e39bff8f6ff8e094618e85d3975538f8223
# Parent  6ffbc7b11abd096c52ce5aed1fc96ad494c0308b
tuned simp trace;

diff -r 6ffbc7b11abd -r bd686e39bff8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 30 09:54:47 1997 +0100
+++ b/src/Pure/thm.ML	Thu Oct 30 09:59:38 1997 +0100
@@ -1650,7 +1650,7 @@
 
 fun add_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
     (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
-  (trace_term ("Adding simplification procedure " ^ name ^ " for:")
+  (trace_term ("Adding simplification procedure " ^ quote name ^ " for:")
       (Sign.deref sign_ref) t;
     mk_mss (rules, congs,
       Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
@@ -1832,11 +1832,11 @@
       fun proc_rews _ ([]:simproc list) = None
         | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
             if Pattern.matches tsigt (plhs, t) then
-             (trace_term ("Trying procedure " ^ name ^ " on:") signt eta_t;
+             (trace_term ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
               case proc signt prems eta_t of
                 None => (trace "FAILED"; proc_rews eta_t ps)
               | Some raw_thm =>
-                 (trace_thm ("Procedure " ^ name ^ " proved rewrite rule:") raw_thm;
+                 (trace_thm ("Procedure " ^ quote name ^ " proved rewrite rule:") raw_thm;
                    (case rews (mk_procrule raw_thm) of
                      None => (trace "IGNORED"; proc_rews eta_t ps)
                    | some => some)))