author | nipkow |
Tue, 21 Jun 1994 11:55:36 +0200 | |
changeset 433 | 1e4f420523ae |
parent 432 | 0d1071ac599c |
child 434 | 89d45187f04d |
--- 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,