improved error msg
authornipkow
Tue, 21 Jun 1994 11:55:36 +0200
changeset 433 1e4f420523ae
parent 432 0d1071ac599c
child 434 89d45187f04d
improved error msg
src/Provers/simplifier.ML
--- 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,