# HG changeset patch
# User huffman
# Date 1274578478 25200
# Node ID 476016cbf8b31c7427cd9f55fdfcfb9590b6ca9c
# Parent  7b74b4a734fd9641ca329f7773a9ece7c4af2348
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run

diff -r 7b74b4a734fd -r 476016cbf8b3 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat May 22 17:57:16 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Sat May 22 18:34:38 2010 -0700
@@ -78,9 +78,16 @@
   in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
 
 fun mk_run t =
-  let val mT = Term.fastype_of t
-      val T = dest_matchT mT
-  in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
+  let
+    val mT = Term.fastype_of t
+    val T = dest_matchT mT
+    val run = Const(@{const_name Fixrec.run}, mT ->> T)
+  in
+    case t of
+      Const(@{const_name Rep_CFun}, _) $
+        Const(@{const_name Fixrec.return}, _) $ u => u
+    | _ => run ` t
+  end;
 
 
 (*************************************************************************)
@@ -129,7 +136,7 @@
         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" ^
+          "or simp rules are configured for all non-HOLCF constants.\n" ^
           "The error occurred for the goal statement:\n" ^
           Syntax.string_of_term lthy prop);
         val rules = Cont2ContData.get lthy;