# HG changeset patch
# User huffman
# Date 1274299635 25200
# Node ID 63fadc0a33db3b2a3f9b86b076de83b2cdcb3421
# Parent  942532de16f62c23366c2b653416cfc917f8ed8d
more informative error message for fixrec when continuity proof fails

diff -r 942532de16f6 -r 63fadc0a33db src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Wed May 19 17:39:22 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Wed May 19 13:07:15 2010 -0700
@@ -125,10 +125,20 @@
     val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
     val functional = lambda_tuple lhss (mk_tuple rhss);
     val fixpoint = mk_fix (mk_cabs functional);
-    
+
     val cont_thm =
-      Goal.prove lthy [] [] (mk_trp (mk_cont functional))
-        (K (simp_tac (simpset_of lthy) 1));
+      let
+        val prop = mk_trp (mk_cont functional);
+        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 tac = simp_tac (simpset_of lthy) 1 THEN check;
+      in
+        Goal.prove lthy [] [] prop (K tac)
+      end;
 
     fun one_def (l as Free(n,_)) r =
           let val b = Long_Name.base_name n