merged
authorwenzelm
Thu, 11 Dec 2008 17:04:46 +0100
changeset 29065 d53f78cafb86
parent 29063 7619f0561cd7 (diff)
parent 29064 70a61d58460e (current diff)
child 29066 f50c24e5b9fe
merged
--- a/src/HOL/Import/HOL4Compat.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -3,7 +3,7 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-theory HOL4Compat imports HOL4Setup Divides Primes Real 
+theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
 begin
 
 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
--- a/src/HOL/Int.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Int.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -761,41 +761,18 @@
 
 text {* Subtraction *}
 
-lemma diff_Pls:
-  "Pls - k = - k"
-  unfolding numeral_simps by simp
-
-lemma diff_Min:
-  "Min - k = pred (- k)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit0:
+lemma diff_bin_simps [simp]:
+  "k - Pls = k"
+  "k - Min = succ k"
+  "Pls - (Bit0 l) = Bit0 (Pls - l)"
+  "Pls - (Bit1 l) = Bit1 (Min - l)"
+  "Min - (Bit0 l) = Bit1 (Min - l)"
+  "Min - (Bit1 l) = Bit0 (Min - l)"
   "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit1:
   "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit0:
   "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit1:
   "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Pls_right:
-  "k - Pls = k"
-  unfolding numeral_simps by simp
-
-lemma diff_Min_right:
-  "k - Min = succ k"
-  unfolding numeral_simps by simp
-
-lemmas diff_bin_simps [simp] =
-  diff_Pls diff_Min diff_Pls_right diff_Min_right
-  diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1
+  unfolding numeral_simps by simp_all
 
 text {* Multiplication *}
 
--- a/src/HOL/IntDiv.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/IntDiv.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -1472,6 +1472,29 @@
   IntDiv.zpower_zmod
   zminus_zmod zdiff_zmod_left zdiff_zmod_right
 
+text {* Distributive laws for function @{text nat}. *}
+
+lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
+apply (rule linorder_cases [of y 0])
+apply (simp add: div_nonneg_neg_le0)
+apply simp
+apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
+done
+
+(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
+lemma nat_mod_distrib:
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
+apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO)
+apply (simp add: nat_eq_iff zmod_int)
+done
+
+text{*Suggested by Matthias Daum*}
+lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
+apply (rule Divides.div_less_dividend, simp_all)
+done
+
 text {* code generator setup *}
 
 context ring_1
--- a/src/HOL/NatBin.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/NatBin.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -118,52 +118,8 @@
 done
 
 
-text{*Distributive laws for type @{text nat}.  The others are in theory
-   @{text IntArith}, but these require div and mod to be defined for type
-   "int".  They also need some of the lemmas proved above.*}
-
-lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
-apply (case_tac "0 <= z'")
-apply (auto simp add: div_nonneg_neg_le0)
-apply (case_tac "z' = 0", simp)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
- prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
-apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-done
-
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib:
-     "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
- prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
-apply (rule int_int_eq [THEN iffD1], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-done
-
-text{*Suggested by Matthias Daum*}
-lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp (asm_lr) add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all) 
-done
-
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma int_nat_number_of [simp]:
      "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
@@ -195,7 +151,6 @@
 
 subsubsection{*Addition *}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma add_nat_number_of [simp]:
      "(number_of v :: nat) + number_of v' =  
          (if v < Int.Pls then number_of v'  
@@ -303,7 +258,6 @@
      "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
 by (auto elim!: nonneg_eq_int)
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma eq_nat_number_of [simp]:
      "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -6,7 +6,7 @@
 header {* Bounds *}
 
 theory Bounds
-imports Main Real
+imports Main ContNotDenum
 begin
 
 locale lub =
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -93,9 +93,11 @@
     end
 
 
-fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
     let
-      val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
+      val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
+      val ((fixes0, spec0), ctxt') = 
+        prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
       val fixes = map (apfst (apfst Binding.base_name)) fixes0;
       val spec = map (apfst (apfst Binding.base_name)) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
@@ -160,8 +162,9 @@
   |> LocalTheory.set_group (serial_string ())
   |> setup_termination_proof term_opt;
 
-val add_fundef = gen_add_fundef true Specification.read_specification
-val add_fundef_i = gen_add_fundef false Specification.check_specification
+val add_fundef = gen_add_fundef true Specification.read_specification "_::type"
+val add_fundef_i = 
+  gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)
--- a/src/HOL/Tools/typedef_package.ML	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/typedef_package.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Gordon/HOL-style type definitions: create a new syntactic type
@@ -9,10 +8,10 @@
 signature TYPEDEF_PACKAGE =
 sig
   type info =
-   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
-    inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
-    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
-    Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
+   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
+    type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
+    Rep_induct: thm, Abs_induct: thm}
   val get_info: theory -> string -> info option
   val add_typedef: bool -> string option -> bstring * string list * mixfix ->
     term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
@@ -27,31 +26,15 @@
 structure TypedefPackage: TYPEDEF_PACKAGE =
 struct
 
-(** theory context references **)
-
-val type_definitionN = "Typedef.type_definition";
-
-val Rep = @{thm "type_definition.Rep"};
-val Rep_inverse = @{thm "type_definition.Rep_inverse"};
-val Abs_inverse = @{thm "type_definition.Abs_inverse"};
-val Rep_inject = @{thm "type_definition.Rep_inject"};
-val Abs_inject = @{thm "type_definition.Abs_inject"};
-val Rep_cases = @{thm "type_definition.Rep_cases"};
-val Abs_cases = @{thm "type_definition.Abs_cases"};
-val Rep_induct = @{thm "type_definition.Rep_induct"};
-val Abs_induct = @{thm "type_definition.Abs_induct"};
-
-
-
 (** type definitions **)
 
 (* theory data *)
 
 type info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
-  inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
-  Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
-  Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
+ {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
+  type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+  Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
+  Rep_induct: thm, Abs_induct: thm};
 
 structure TypedefData = TheoryDataFun
 (
@@ -90,10 +73,6 @@
     val rhs_tfreesT = Term.add_tfreesT setT [];
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
       error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
-    fun mk_inhabited A =
-      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
-    val goal = mk_inhabited set;
-    val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
 
     (*lhs*)
     val defS = Sign.defaultS thy;
@@ -111,59 +90,71 @@
     val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
     val RepC = Const (full Rep_name, newT --> oldT);
     val AbsC = Const (full Abs_name, oldT --> newT);
-    val x_new = Free ("x", newT);
-    val y_old = Free ("y", oldT);
 
+    (*inhabitance*)
+    fun mk_inhabited A =
+      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
     val set' = if def then setC else set;
+    val goal' = mk_inhabited set';
+    val goal = mk_inhabited set;
+    val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
 
+    (*axiomatization*)
     val typedef_name = "type_definition_" ^ name;
     val typedefC =
-      Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
-    val typedef_prop =
-      Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
+      Const (@{const_name type_definition},
+        (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
+    val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
     val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
 
-    fun add_def eq thy =
+    (*set definition*)
+    fun add_def theory =
       if def then
-        thy
-        |> PureThy.add_defs false [Thm.no_attributes eq]
+        theory
+        |> Sign.add_consts_i [(name, setT', NoSyn)]
+        |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))]
         |-> (fn [th] => pair (SOME th))
-      else (NONE, thy);
+      else (NONE, theory);
+    fun contract_def NONE th = th
+      | contract_def (SOME def_eq) th =
+          let
+            val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
+            val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
+          in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
       ObjectLogic.typedecl (t, vs, mx)
       #> snd
       #> Sign.add_consts_i
-       ((if def then [(name, setT', NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
-         (Abs_name, oldT --> newT, NoSyn)])
-      #> add_def (PrimitiveDefs.mk_defpair (setC, set))
-      ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
-          [apsnd (fn cond_axm => inhabited RS cond_axm)])]
+         (Abs_name, oldT --> newT, NoSyn)]
+      #> add_def
+      #-> (fn set_def =>
+        PureThy.add_axioms [((typedef_name, typedef_prop),
+          [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
+        ##>> pair set_def)
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
-      #-> (fn (set_def, [type_definition]) => fn thy1 =>
+      #-> (fn ([type_definition], set_def) => fn thy1 =>
         let
           fun make th = Drule.standard (th OF [type_definition]);
-          val abs_inject = make Abs_inject;
-          val abs_inverse = make Abs_inverse;
           val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
             thy1
             |> Sign.add_path name
             |> PureThy.add_thms
-              ([((Rep_name, make Rep), []),
-                ((Rep_name ^ "_inverse", make Rep_inverse), []),
-                ((Abs_name ^ "_inverse", abs_inverse), []),
-                ((Rep_name ^ "_inject", make Rep_inject), []),
-                ((Abs_name ^ "_inject", abs_inject), []),
-                ((Rep_name ^ "_cases", make Rep_cases),
+              ([((Rep_name, make @{thm type_definition.Rep}), []),
+                ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
+                ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
+                ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
+                ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
+                ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
                   [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
-                ((Abs_name ^ "_cases", make Abs_cases),
+                ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
                   [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
-                ((Rep_name ^ "_induct", make Rep_induct),
+                ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
                   [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
-                ((Abs_name ^ "_induct", make Abs_induct),
+                ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
                   [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
             ||> Sign.parent_path;
           val info = {rep_type = oldT, abs_type = newT,
@@ -212,20 +203,20 @@
   handle ERROR msg => err_in_typedef msg name;
 
 
-(* add_typedef interface *)
+(* add_typedef: tactic interface *)
 
 fun add_typedef def opt_name typ set opt_morphs tac thy =
   let
     val name = the_default (#1 typ) opt_name;
     val (set, goal, _, typedef_result) =
       prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
-    val non_empty = Goal.prove_global thy [] [] goal (K tac)
+    val inhabited = Goal.prove_global thy [] [] goal (K tac)
       handle ERROR msg => cat_error msg
         ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
-  in typedef_result non_empty thy end;
+  in typedef_result inhabited thy end;
 
 
-(* Isar typedef interface *)
+(* typedef: proof interface *)
 
 local
 
@@ -247,7 +238,7 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = OuterParse in
 
 val _ = OuterKeyword.keyword "morphisms";
 
@@ -262,11 +253,13 @@
   typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
 
 val _ =
-  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
+  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
+    OuterKeyword.thy_goal
     (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
 
+end;
+
+
 val setup = TypedefInterpretation.init;
 
 end;
-
-end;
--- a/src/HOL/Typedef.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Typedef.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Typedef.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Munich
 *)
 
@@ -116,15 +115,10 @@
 
 end
 
-use "Tools/typedef_package.ML"
-use "Tools/typecopy_package.ML"
-use "Tools/typedef_codegen.ML"
+use "Tools/typedef_package.ML" setup TypedefPackage.setup
+use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
+use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
 
-setup {*
-  TypedefPackage.setup
-  #> TypecopyPackage.setup
-  #> TypedefCodegen.setup
-*}
 
 text {* This class is just a workaround for classes without parameters;
   it shall disappear as soon as possible. *}
--- a/src/HOL/ex/MIR.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/ex/MIR.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -1,9 +1,9 @@
-(*  Title:      Complex/ex/MIR.thy
+(*  Title:      HOL/ex/MIR.thy
     Author:     Amine Chaieb
 *)
 
 theory MIR
-imports List Real Code_Integer Efficient_Nat
+imports Main RComplete Code_Integer Efficient_Nat
 uses ("mirtac.ML")
 begin
 
--- a/src/HOLCF/Cfun.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -23,7 +23,7 @@
 by (rule admI, rule cont_lub_fun)
 
 cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
-by (simp add: Ex_cont adm_cont)
+by (simp_all add: Ex_cont adm_cont)
 
 syntax (xsymbols)
   "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
@@ -303,31 +303,34 @@
 text {* cont2cont lemma for @{term Rep_CFun} *}
 
 lemma cont2cont_Rep_CFun:
-  "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x)\<cdot>(t x))"
-by (best intro: cont2cont_app2 cont_const cont_Rep_CFun cont_Rep_CFun2)
+  assumes f: "cont (\<lambda>x. f x)"
+  assumes t: "cont (\<lambda>x. t x)"
+  shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
+proof -
+  have "cont (\<lambda>x. Rep_CFun (f x))"
+    using cont_Rep_CFun f by (rule cont2cont_app3)
+  thus "cont (\<lambda>x. (f x)\<cdot>(t x))"
+    using cont_Rep_CFun2 t by (rule cont2cont_app2)
+qed
 
 text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
 
 lemma cont2mono_LAM:
-assumes p1: "!!x. cont(c1 x)"
-assumes p2: "!!y. monofun(%x. c1 x y)"
-shows "monofun(%x. LAM y. c1 x y)"
-apply (rule monofunI)
-apply (rule less_cfun_ext)
-apply (simp add: p1)
-apply (erule p2 [THEN monofunE])
-done
+  "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
+    \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
+  unfolding monofun_def expand_cfun_less by simp
 
-text {* cont2cont Lemma for @{term "%x. LAM y. c1 x y"} *}
+text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
 
 lemma cont2cont_LAM:
-assumes p1: "!!x. cont(c1 x)"
-assumes p2: "!!y. cont(%x. c1 x y)"
-shows "cont(%x. LAM y. c1 x y)"
-apply (rule cont_Abs_CFun)
-apply (simp add: p1 CFun_def)
-apply (simp add: p2 cont2cont_lambda)
-done
+  assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
+  assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
+  shows "cont (\<lambda>x. \<Lambda> y. f x y)"
+proof (rule cont_Abs_CFun)
+  fix x
+  from f1 show "f x \<in> CFun" by (simp add: CFun_def)
+  from f2 show "cont f" by (rule cont2cont_lambda)
+qed
 
 text {* continuity simplification procedure *}
 
--- a/src/HOLCF/Fixrec.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Fixrec.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -15,7 +15,7 @@
 defaultsort cpo
 
 pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
-by simp
+by simp_all
 
 constdefs
   fail :: "'a maybe"
--- a/src/HOLCF/Lift.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Lift.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -12,7 +12,7 @@
 defaultsort type
 
 pcpodef 'a lift = "UNIV :: 'a discr u set"
-by simp
+by simp_all
 
 instance lift :: (finite) finite_po
 by (rule typedef_finite_po [OF type_definition_lift])
--- a/src/HOLCF/Sprod.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Sprod.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -17,7 +17,7 @@
 
 pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
         "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
-by simp
+by simp_all
 
 instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
 by (rule typedef_finite_po [OF type_definition_Sprod])
--- a/src/HOLCF/Ssum.thy	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Thu Dec 11 17:04:46 2008 +0100
@@ -19,7 +19,7 @@
   "{p :: tr \<times> ('a \<times> 'b).
     (cfst\<cdot>p \<sqsubseteq> TT \<longleftrightarrow> csnd\<cdot>(csnd\<cdot>p) = \<bottom>) \<and>
     (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
-by simp
+by simp_all
 
 instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
 by (rule typedef_finite_po [OF type_definition_Ssum])
--- a/src/HOLCF/Tools/cont_proc.ML	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Tools/cont_proc.ML
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -8,7 +7,7 @@
   val is_lcf_term: term -> bool
   val cont_thms: term -> thm list
   val all_cont_thms: term -> thm list
-  val cont_tac: int -> tactic
+  val cont_tac: thm list ref -> int -> tactic
   val cont_proc: theory -> simproc
   val setup: theory -> theory
 end;
@@ -16,13 +15,22 @@
 structure ContProc: CONT_PROC =
 struct
 
+structure ContProcData = TheoryDataFun
+(
+  type T = thm list ref;
+  val empty = ref [];
+  val copy = I;
+  val extend = I;
+  fun merge _ _ = ref [];
+)
+
 (** theory context references **)
 
-val cont_K = thm "cont_const";
-val cont_I = thm "cont_id";
-val cont_A = thm "cont2cont_Rep_CFun";
-val cont_L = thm "cont2cont_LAM";
-val cont_R = thm "cont_Rep_CFun2";
+val cont_K = @{thm cont_const};
+val cont_I = @{thm cont_id};
+val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_L = @{thm cont2cont_LAM};
+val cont_R = @{thm cont_Rep_CFun2};
 
 (* checks whether a term contains no dangling bound variables *)
 val is_closed_term =
@@ -35,10 +43,11 @@
   in bound_less 0 end;
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) =
+fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t
-  | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+      is_lcf_term t
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ _) = false
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = is_closed_term t;
 
@@ -73,12 +82,12 @@
   (* first list: cont thm for each dangling bound variable *)
   (* second list: cont thm for each LAM in t *)
   (* if b = false, only return cont thm for outermost LAMs *)
-  fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) $ f $ t) =
+  fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) $ f $ t) =
     let
       val (cs1,ls1) = cont_thms1 b f;
       val (cs2,ls2) = cont_thms1 b t;
     in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
-    | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) =
+    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
     let
       val (cs, ls) = cont_thms1 b t;
       val (cs', l) = lam cs;
@@ -98,41 +107,40 @@
   conditional rewrite rule with the unsolved subgoals as premises.
 *)
 
-local
-  val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
+fun cont_tac prev_cont_thms =
+  let
+    val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
   
-  (* FIXME proper cache as theory data!? *)
-  val prev_cont_thms : thm list ref = ref [];
+    fun old_cont_tac i thm =
+      case !prev_cont_thms of
+        [] => no_tac thm
+      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
 
-  fun old_cont_tac i thm = CRITICAL (fn () =>
-    case !prev_cont_thms of
-      [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
+    fun new_cont_tac f' i thm =
+      case all_cont_thms f' of
+        [] => no_tac thm
+      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
 
-  fun new_cont_tac f' i thm = CRITICAL (fn () =>
-    case all_cont_thms f' of
-      [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
-
-  fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
-    let
-      val f' = Const ("Cfun.Abs_CFun", dummyT) $ f;
-    in
-      if is_lcf_term f'
-      then old_cont_tac ORELSE' new_cont_tac f'
-      else REPEAT_ALL_NEW (resolve_tac rules)
-    end
-    | cont_tac_of_term _ = K no_tac;
-in
-  val cont_tac =
-    SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
-end;
+    fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
+      let
+        val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
+      in
+        if is_lcf_term f'
+        then old_cont_tac ORELSE' new_cont_tac f'
+        else REPEAT_ALL_NEW (resolve_tac rules)
+      end
+      | cont_tac_of_term _ = K no_tac;
+  in
+    SUBGOAL (fn (t, i) =>
+      cont_tac_of_term (HOLogic.dest_Trueprop t) i)
+  end;
 
 local
   fun solve_cont thy _ t =
     let
       val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
-    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
+      val prev_thms = ContProcData.get thy
+    in Option.map fst (Seq.pull (cont_tac prev_thms 1 tr)) end
 in
   fun cont_proc thy =
     Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
--- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -1,44 +1,25 @@
 (*  Title:      HOLCF/Tools/pcpodef_package.ML
-    ID:         $Id$
     Author:     Brian Huffman
 
 Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef.
+typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
 *)
 
 signature PCPODEF_PACKAGE =
 sig
-  val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
+  val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
-  val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+  val pcpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
     * (string * string) option -> theory -> Proof.state
-  val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
+  val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
-  val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+  val cpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
     * (string * string) option -> theory -> Proof.state
 end;
 
 structure PcpodefPackage: PCPODEF_PACKAGE =
 struct
 
-(** theory context references **)
-
-val typedef_po = thm "typedef_po";
-val typedef_cpo = thm "typedef_cpo";
-val typedef_pcpo = thm "typedef_pcpo";
-val typedef_lub = thm "typedef_lub";
-val typedef_thelub = thm "typedef_thelub";
-val typedef_compact = thm "typedef_compact";
-val cont_Rep = thm "typedef_cont_Rep";
-val cont_Abs = thm "typedef_cont_Abs";
-val Rep_strict = thm "typedef_Rep_strict";
-val Abs_strict = thm "typedef_Abs_strict";
-val Rep_strict_iff = thm "typedef_Rep_strict_iff";
-val Abs_strict_iff = thm "typedef_Abs_strict_iff";
-val Rep_defined = thm "typedef_Rep_defined";
-val Abs_defined = thm "typedef_Abs_defined";
-
-
 (** type definitions **)
 
 (* prepare_cpodef *)
@@ -48,11 +29,12 @@
 
 fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
 
-fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
+fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
 
 fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
   let
+    val _ = Theory.requires thy "Pcpodef" "pcpodefs";
     val ctxt = ProofContext.init thy;
     val full = Sign.full_bname thy;
 
@@ -60,29 +42,29 @@
     val full_name = full name;
     val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
     val setT = Term.fastype_of set;
-    val rhs_tfrees = term_tfrees set;
+    val rhs_tfrees = Term.add_tfrees set [];
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
       error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
-    fun mk_nonempty A =
-      HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
-    fun mk_admissible A =
-      mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
-    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
-    val goal = if pcpo
-      then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
-      else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
+
+    (*goal*)
+    val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+    val goal_nonempty =
+      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+    val goal_admissible =
+      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
 
     (*lhs*)
     val defS = Sign.defaultS thy;
     val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
     val lhs_sorts = map snd lhs_tfrees;
+
     val tname = Syntax.type_name t mx;
     val full_tname = full tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
     val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
     val RepC = Const (full Rep_name, newT --> oldT);
-    fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT);
+    fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
     val less_def = Logic.mk_equals (lessC newT,
       Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
 
@@ -91,7 +73,7 @@
         val ((_, {type_definition, set_def, ...}), thy2) = thy1
           |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
         val lthy3 = thy2
-          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
+          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
         val less_def' = Syntax.check_term lthy3 less_def;
         val ((_, (_, less_definition')), lthy4) = lthy3
           |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
@@ -99,7 +81,7 @@
         val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
         val thy5 = lthy4
           |> Class.prove_instantiation_instance
-              (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
+              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, less_definition]) 1))
           |> LocalTheory.exit_global;
       in ((type_definition, less_definition, set_def), thy5) end;
 
@@ -108,91 +90,88 @@
         val admissible' = fold_rule (the_list set_def) admissible;
         val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible'];
         val theory' = theory
-          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
-            (Tactic.rtac (typedef_cpo OF cpo_thms) 1);
+          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
+            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
         val cpo_thms' = map (Thm.transfer theory') cpo_thms;
       in
         theory'
         |> Sign.add_path name
         |> PureThy.add_thms
-            ([(("adm_" ^ name, admissible'), []),
-              (("cont_" ^ Rep_name, cont_Rep OF cpo_thms'), []),
-              (("cont_" ^ Abs_name, cont_Abs OF cpo_thms'), []),
-              (("lub_"     ^ name, typedef_lub     OF cpo_thms'), []),
-              (("thelub_"  ^ name, typedef_thelub  OF cpo_thms'), []),
-              (("compact_" ^ name, typedef_compact OF cpo_thms'), [])])
+          ([(("adm_" ^ name, admissible'), []),
+            (("cont_" ^ Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
+            (("cont_" ^ Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
+            (("lub_" ^ name, @{thm typedef_lub} OF cpo_thms'), []),
+            (("thelub_" ^ name, @{thm typedef_thelub} OF cpo_thms'), []),
+            (("compact_" ^ name, @{thm typedef_compact} OF cpo_thms'), [])])
         |> snd
         |> Sign.parent_path
       end;
 
-    fun make_pcpo UUmem (type_def, less_def, set_def) theory =
+    fun make_pcpo UU_mem (type_def, less_def, set_def) theory =
       let
-        val UUmem' = fold_rule (the_list set_def) UUmem;
-        val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UUmem'];
+        val UU_mem' = fold_rule (the_list set_def) UU_mem;
+        val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem'];
         val theory' = theory
-          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
-            (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1);
+          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
+            (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
         val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
       in
         theory'
         |> Sign.add_path name
         |> PureThy.add_thms
-            ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms'), []),
-              ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms'), []),
-              ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms'), []),
-              ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms'), []),
-              ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms'), []),
-              ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms'), [])
+            ([((Rep_name ^ "_strict", @{thm typedef_Rep_strict} OF pcpo_thms'), []),
+              ((Abs_name ^ "_strict", @{thm typedef_Abs_strict} OF pcpo_thms'), []),
+              ((Rep_name ^ "_strict_iff", @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
+              ((Abs_name ^ "_strict_iff", @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
+              ((Rep_name ^ "_defined", @{thm typedef_Rep_defined} OF pcpo_thms'), []),
+              ((Abs_name ^ "_defined", @{thm typedef_Abs_defined} OF pcpo_thms'), [])
               ])
         |> snd
         |> Sign.parent_path
       end;
 
-    fun pcpodef_result UUmem_admissible theory =
-      let
-        val UUmem = UUmem_admissible RS conjunct1;
-        val admissible = UUmem_admissible RS conjunct2;
-      in
-        theory
-        |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
-        |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs)
-      end;
+    fun pcpodef_result UU_mem admissible =
+      make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
+      #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
 
-    fun cpodef_result nonempty_admissible theory =
-      let
-        val nonempty = nonempty_admissible RS conjunct1;
-        val admissible = nonempty_admissible RS conjunct2;
-      in
-        theory
-        |> make_po (Tactic.rtac nonempty 1)
-        |-> make_cpo admissible
-      end;
-
-  in (goal, if pcpo then pcpodef_result else cpodef_result) end
+    fun cpodef_result nonempty admissible =
+      make_po (Tactic.rtac nonempty 1)
+      #-> make_cpo admissible;
+  in
+    if pcpo
+    then (goal_UU_mem, goal_admissible, pcpodef_result)
+    else (goal_nonempty, goal_admissible, cpodef_result)
+  end
   handle ERROR msg => err_in_cpodef msg name;
 
 
-(* cpodef_proof interface *)
+(* proof interface *)
+
+local
 
 fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
   let
-    val (goal, pcpodef_result) =
+    val (goal1, goal2, make_result) =
       prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
-    fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
-  in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
+    fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
+  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
+
+in
 
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x;
-fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x;
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
 
-fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x;
-fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x;
+fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
+fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
+
+end;
+
 
 
 (** outer syntax **)
 
 local structure P = OuterParse and K = OuterKeyword in
 
-(* cf. HOL/Tools/typedef_package.ML *)
 val typedef_proof_decl =
   Scan.optional (P.$$$ "(" |--
       ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
@@ -201,7 +180,7 @@
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
 
 fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
-  (if pcpo then pcpodef_proof else cpodef_proof)
+  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
     ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
 
 val _ =