src/Pure/simplifier.ML
changeset 46465 5ba52c337cd0
parent 45625 750c5a47400b
child 46776 8575cc482dfb
equal deleted inserted replaced
46464:4cf5a84e2c05 46465:5ba52c337cd0
   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