changeset 46465 | 5ba52c337cd0 |
parent 45625 | 750c5a47400b |
child 46776 | 8575cc482dfb |
--- a/src/Pure/simplifier.ML Tue Feb 14 19:18:57 2012 +0100 +++ b/src/Pure/simplifier.ML Tue Feb 14 19:29:54 2012 +0100 @@ -239,7 +239,7 @@ (rev (if safe then solvers else unsafe_solvers))); fun simp_loop_tac i = - Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN + Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); in simp_loop_tac end;