src/Provers/simplifier.ML
changeset 433 1e4f420523ae
parent 406 4d4e0442b106
child 983 6f80fed73e29
--- a/src/Provers/simplifier.ML	Mon Jun 20 12:25:28 1994 +0200
+++ b/src/Provers/simplifier.ML	Tue Jun 21 11:55:36 1994 +0200
@@ -54,7 +54,7 @@
      congs= congs,
      subgoal_tac= subgoal_tac,
      finish_tac=finish_tac,
-     loop_tac=loop_tac};
+     loop_tac= DETERM o loop_tac};
 
 fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
   SS{mss=mss,