# HG changeset patch
# User huffman
# Date 1274576236 25200
# Node ID 7b74b4a734fd9641ca329f7773a9ece7c4af2348
# Parent  dd47971b987565c252ba69f9233969d86ad802cd
simplify fixrec continuity tactic

diff -r dd47971b9875 -r 7b74b4a734fd src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat May 22 17:44:12 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Sat May 22 17:57:16 2010 -0700
@@ -127,16 +127,15 @@
     val cont_thm =
       let
         val prop = mk_trp (mk_cont functional);
-        fun err () = error (
+        fun err _ = error (
           "Continuity proof failed; please check that cont2cont rules\n" ^
           "are configured for all non-HOLCF constants.\n" ^
           "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 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;
+        val slow_tac = SOLVED' (simp_tac (simpset_of lthy));
+        val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err;
       in
         Goal.prove lthy [] [] prop (K tac)
       end;