merged

--- a/src/HOLCF/Cont.thy	Sun May 23 22:56:45 2010 +0200
+++ b/src/HOLCF/Cont.thy	Sun May 23 19:30:29 2010 -0700
@@ -178,7 +178,7 @@
 
 text {* if-then-else is continuous *}
 
-lemma cont_if [simp]:
+lemma cont_if [simp, cont2cont]:
   "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
 by (induct b) simp_all
 

--- a/src/HOLCF/Lift.thy	Sun May 23 22:56:45 2010 +0200
+++ b/src/HOLCF/Lift.thy	Sun May 23 19:30:29 2010 -0700
@@ -137,7 +137,7 @@
 apply (simp add: below_fun_ext)
 done
 
-lemma cont2cont_flift1 [simp]:
+lemma cont2cont_flift1 [simp, cont2cont]:
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
 apply (rule cont_flift1 [THEN cont2cont_app3])
 apply simp

--- a/src/HOLCF/Tools/cont_consts.ML	Sun May 23 22:56:45 2010 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML	Sun May 23 19:30:29 2010 -0700
@@ -90,11 +90,4 @@
 
 end;
 
-
-(* outer syntax *)
-
-val _ =
-  Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
-    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
-
 end;

--- a/src/HOLCF/Tools/fixrec.ML	Sun May 23 22:56:45 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Sun May 23 19:30:29 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;
 
 
 (*************************************************************************)
@@ -127,16 +134,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" ^
+          "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);
-        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;