equal
deleted
inserted
replaced
237 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
237 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
238 val solve_tac = FIRST' (map (Raw_Simplifier.solver ss) |
238 val solve_tac = FIRST' (map (Raw_Simplifier.solver ss) |
239 (rev (if safe then solvers else unsafe_solvers))); |
239 (rev (if safe then solvers else unsafe_solvers))); |
240 |
240 |
241 fun simp_loop_tac i = |
241 fun simp_loop_tac i = |
242 Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN |
242 Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN |
243 (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
243 (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
244 in simp_loop_tac end; |
244 in simp_loop_tac end; |
245 |
245 |
246 local |
246 local |
247 |
247 |