# HG changeset patch
# User nipkow
# Date 772192536 -7200
# Node ID 1e4f420523ae1fd299f0767c32184698d8c4f891
# Parent  0d1071ac599c04631d0a38b47d2c3cce0a7bff40
improved error msg

diff -r 0d1071ac599c -r 1e4f420523ae 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,