# HG changeset patch # User wenzelm # Date 1334416557 -7200 # Node ID 402b753d83834344b93f250bad95897af463e309 # Parent a0007b769a34050b43d9b850885643de7d17c4a5 outermost SELECT_GOAL potentially improves performance; diff -r a0007b769a34 -r 402b753d8383 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Apr 14 16:40:17 2012 +0200 +++ b/src/Pure/simplifier.ML Sat Apr 14 17:15:57 2012 +0200 @@ -240,7 +240,7 @@ fun simp_loop_tac i = 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; + in SELECT_GOAL (simp_loop_tac 1) end; local