1.1 --- a/src/HOLCF/Tools/fixrec.ML	Sat May 22 13:40:15 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sat May 22 14:04:05 2010 -0700
     1.3 @@ -133,7 +133,10 @@
     1.4            "The error occurred for the goal statement:\n" ^
     1.5            Syntax.string_of_term lthy prop);
     1.6          fun check th = case Thm.nprems_of th of 0 => all_tac th | n => err ();
     1.7 -        val tac = simp_tac (simpset_of lthy) 1 THEN check;
     1.8 +        val rules = Cont2ContData.get lthy;
     1.9 +        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
    1.10 +        val slow_tac = simp_tac (simpset_of lthy);
    1.11 +        val tac = (fast_tac 1 ORELSE slow_tac 1) THEN check;
    1.12        in
    1.13          Goal.prove lthy [] [] prop (K tac)
    1.14        end;