Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
outermost SELECT_GOAL potentially improves performance;
authorwenzelm
Sat, 14 Apr 2012 17:15:57 +0200
changeset 47468 402b753d8383
parent 47467 a0007b769a34
child 47469 ba7fe841c885
outermost SELECT_GOAL potentially improves performance;
src/Pure/simplifier.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle