1.1 --- a/src/Pure/simplifier.ML	Sat Apr 14 16:40:17 2012 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Sat Apr 14 17:15:57 2012 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4      fun simp_loop_tac i =
     1.5        Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
     1.6        (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
     1.7 -  in simp_loop_tac end;
     1.8 +  in SELECT_GOAL (simp_loop_tac 1) end;
     1.9  
    1.10  local
    1.11