# HG changeset patch
# User wenzelm
# Date 964560793 -7200
# Node ID 7bc054e9fb1c8ecef3a937262675f29c21fb1800
# Parent  6c93b1eb11f87d9c092407e4457910df89a8916f
tuned msg;

diff -r 6c93b1eb11f8 -r 7bc054e9fb1c src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Jul 25 18:43:52 2000 +0200
+++ b/src/Provers/simplifier.ML	Tue Jul 25 23:33:13 2000 +0200
@@ -185,12 +185,12 @@
 
 fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
     setloop tac =
-  make_ss (mss, subgoal_tac, [("",tac)], unsafe_solvers, solvers);
+  make_ss (mss, subgoal_tac, [("", tac)], unsafe_solvers, solvers);
 
 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
     addloop tac = make_ss (mss, subgoal_tac, 
-        (case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => 
-         warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)),
+        (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x => 
+         warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac)),
            unsafe_solvers, solvers);
 
 fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})