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,