src/HOLCF/Tools/fixrec.ML
changeset 37108 00f13d3ad474
parent 37097 476016cbf8b3
child 39557 fe5722fce758
--- a/src/HOLCF/Tools/fixrec.ML	Mon May 24 13:48:57 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Mon May 24 09:32:52 2010 -0700
@@ -85,7 +85,7 @@
   in
     case t of
       Const(@{const_name Rep_CFun}, _) $
-        Const(@{const_name Fixrec.return}, _) $ u => u
+        Const(@{const_name Fixrec.succeed}, _) $ u => u
     | _ => run ` t
   end;
 
@@ -267,7 +267,7 @@
   let
     val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
   in
-    building match_name lhs (mk_return rhs) [] (taken_names eq)
+    building match_name lhs (mk_succeed rhs) [] (taken_names eq)
   end;
 
 (* returns the sum (using +++) of the terms in ms *)