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.
tuned msg;
authorwenzelm
Tue, 25 Jul 2000 23:33:13 +0200
changeset 9446 7bc054e9fb1c
parent 9445 6c93b1eb11f8
child 9447 e5180c869772
tuned msg;
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- 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})
isabelle