# HG changeset patch
# User huffman
# Date 1274562245 25200
# Node ID 665a3dfe863276320c306966bb4bf8e783ce32df
# Parent  03a70ab79dd96e918479c9328bfbf864c5b1430e
optimize continuity proofs in fixrec package, using cont2cont rules

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