proper names for types cfun, sprod, ssum
authorhuffman
Tue Mar 02 17:21:10 2010 -0800 (2010-03-02)
changeset 35525fa231b86cb1e
parent 35524 a2a59e92b02e
child 35526 85e9423d7deb
proper names for types cfun, sprod, ssum
src/HOLCF/Bifinite.thy
src/HOLCF/Cfun.thy
src/HOLCF/Representable.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/cont_consts.ML
src/HOLCF/Tools/fixrec.ML
src/HOLCF/Tools/holcf_library.ML
src/HOLCF/Tools/repdef.ML
     1.1 --- a/src/HOLCF/Bifinite.thy	Tue Mar 02 17:20:03 2010 -0800
     1.2 +++ b/src/HOLCF/Bifinite.thy	Tue Mar 02 17:21:10 2010 -0800
     1.3 @@ -295,7 +295,7 @@
     1.4      by (rule finite_range_imp_finite_fixes)
     1.5  qed
     1.6  
     1.7 -instantiation "->" :: (profinite, profinite) profinite
     1.8 +instantiation cfun :: (profinite, profinite) profinite
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -325,7 +325,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -instance "->" :: (profinite, bifinite) bifinite ..
    1.17 +instance cfun :: (profinite, bifinite) bifinite ..
    1.18  
    1.19  lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
    1.20  by (simp add: approx_cfun_def)
     2.1 --- a/src/HOLCF/Cfun.thy	Tue Mar 02 17:20:03 2010 -0800
     2.2 +++ b/src/HOLCF/Cfun.thy	Tue Mar 02 17:21:10 2010 -0800
     2.3 @@ -20,11 +20,11 @@
     2.4  lemma adm_cont: "adm cont"
     2.5  by (rule admI, rule cont_lub_fun)
     2.6  
     2.7 -cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
     2.8 +cpodef (CFun)  ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
     2.9  by (simp_all add: Ex_cont adm_cont)
    2.10  
    2.11 -syntax (xsymbols)
    2.12 -  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
    2.13 +type_notation (xsymbols)
    2.14 +  cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
    2.15  
    2.16  notation
    2.17    Rep_CFun  ("(_$/_)" [999,1000] 999)
    2.18 @@ -103,16 +103,16 @@
    2.19  lemma UU_CFun: "\<bottom> \<in> CFun"
    2.20  by (simp add: CFun_def inst_fun_pcpo cont_const)
    2.21  
    2.22 -instance "->" :: (finite_po, finite_po) finite_po
    2.23 +instance cfun :: (finite_po, finite_po) finite_po
    2.24  by (rule typedef_finite_po [OF type_definition_CFun])
    2.25  
    2.26 -instance "->" :: (finite_po, chfin) chfin
    2.27 +instance cfun :: (finite_po, chfin) chfin
    2.28  by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
    2.29  
    2.30 -instance "->" :: (cpo, discrete_cpo) discrete_cpo
    2.31 +instance cfun :: (cpo, discrete_cpo) discrete_cpo
    2.32  by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
    2.33  
    2.34 -instance "->" :: (cpo, pcpo) pcpo
    2.35 +instance cfun :: (cpo, pcpo) pcpo
    2.36  by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
    2.37  
    2.38  lemmas Rep_CFun_strict =
     3.1 --- a/src/HOLCF/Representable.thy	Tue Mar 02 17:20:03 2010 -0800
     3.2 +++ b/src/HOLCF/Representable.thy	Tue Mar 02 17:21:10 2010 -0800
     3.3 @@ -416,7 +416,7 @@
     3.4  
     3.5  text "Functions between representable types are representable."
     3.6  
     3.7 -instantiation "->" :: (rep, rep) rep
     3.8 +instantiation cfun :: (rep, rep) rep
     3.9  begin
    3.10  
    3.11  definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
    3.12 @@ -431,7 +431,7 @@
    3.13  
    3.14  text "Strict products of representable types are representable."
    3.15  
    3.16 -instantiation "**" :: (rep, rep) rep
    3.17 +instantiation sprod :: (rep, rep) rep
    3.18  begin
    3.19  
    3.20  definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
    3.21 @@ -446,7 +446,7 @@
    3.22  
    3.23  text "Strict sums of representable types are representable."
    3.24  
    3.25 -instantiation "++" :: (rep, rep) rep
    3.26 +instantiation ssum :: (rep, rep) rep
    3.27  begin
    3.28  
    3.29  definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
    3.30 @@ -784,13 +784,13 @@
    3.31  
    3.32  setup {*
    3.33    fold Domain_Isomorphism.add_type_constructor
    3.34 -    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
    3.35 +    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
    3.36          @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
    3.37  
    3.38 -     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
    3.39 +     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
    3.40          @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
    3.41  
    3.42 -     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
    3.43 +     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
    3.44          @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
    3.45  
    3.46       (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
     4.1 --- a/src/HOLCF/Sprod.thy	Tue Mar 02 17:20:03 2010 -0800
     4.2 +++ b/src/HOLCF/Sprod.thy	Tue Mar 02 17:21:10 2010 -0800
     4.3 @@ -12,20 +12,20 @@
     4.4  
     4.5  subsection {* Definition of strict product type *}
     4.6  
     4.7 -pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
     4.8 +pcpodef (Sprod)  ('a, 'b) sprod (infixr "**" 20) =
     4.9          "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
    4.10  by simp_all
    4.11  
    4.12 -instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    4.13 +instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    4.14  by (rule typedef_finite_po [OF type_definition_Sprod])
    4.15  
    4.16 -instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    4.17 +instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    4.18  by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
    4.19  
    4.20  syntax (xsymbols)
    4.21 -  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    4.22 +  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    4.23  syntax (HTML output)
    4.24 -  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    4.25 +  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    4.26  
    4.27  lemma spair_lemma:
    4.28    "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
    4.29 @@ -80,11 +80,11 @@
    4.30  apply fast
    4.31  done
    4.32  
    4.33 -lemma sprodE [cases type: **]:
    4.34 +lemma sprodE [cases type: sprod]:
    4.35    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    4.36  by (cut_tac z=p in Exh_Sprod, auto)
    4.37  
    4.38 -lemma sprod_induct [induct type: **]:
    4.39 +lemma sprod_induct [induct type: sprod]:
    4.40    "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
    4.41  by (cases x, simp_all)
    4.42  
    4.43 @@ -221,7 +221,7 @@
    4.44  
    4.45  subsection {* Strict product preserves flatness *}
    4.46  
    4.47 -instance "**" :: (flat, flat) flat
    4.48 +instance sprod :: (flat, flat) flat
    4.49  proof
    4.50    fix x y :: "'a \<otimes> 'b"
    4.51    assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
    4.52 @@ -312,7 +312,7 @@
    4.53  
    4.54  subsection {* Strict product is a bifinite domain *}
    4.55  
    4.56 -instantiation "**" :: (bifinite, bifinite) bifinite
    4.57 +instantiation sprod :: (bifinite, bifinite) bifinite
    4.58  begin
    4.59  
    4.60  definition
     5.1 --- a/src/HOLCF/Ssum.thy	Tue Mar 02 17:20:03 2010 -0800
     5.2 +++ b/src/HOLCF/Ssum.thy	Tue Mar 02 17:21:10 2010 -0800
     5.3 @@ -12,22 +12,22 @@
     5.4  
     5.5  subsection {* Definition of strict sum type *}
     5.6  
     5.7 -pcpodef (Ssum)  ('a, 'b) "++" (infixr "++" 10) = 
     5.8 +pcpodef (Ssum)  ('a, 'b) ssum (infixr "++" 10) = 
     5.9    "{p :: tr \<times> ('a \<times> 'b).
    5.10      (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
    5.11      (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
    5.12  by simp_all
    5.13  
    5.14 -instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    5.15 +instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    5.16  by (rule typedef_finite_po [OF type_definition_Ssum])
    5.17  
    5.18 -instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    5.19 +instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    5.20  by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
    5.21  
    5.22  syntax (xsymbols)
    5.23 -  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    5.24 +  ssum          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    5.25  syntax (HTML output)
    5.26 -  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    5.27 +  ssum          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    5.28  
    5.29  subsection {* Definitions of constructors *}
    5.30  
    5.31 @@ -150,13 +150,13 @@
    5.32  apply (simp add: sinr_Abs_Ssum Ssum_def)
    5.33  done
    5.34  
    5.35 -lemma ssumE [cases type: ++]:
    5.36 +lemma ssumE [cases type: ssum]:
    5.37    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
    5.38     \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
    5.39     \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    5.40  by (cut_tac z=p in Exh_Ssum, auto)
    5.41  
    5.42 -lemma ssum_induct [induct type: ++]:
    5.43 +lemma ssum_induct [induct type: ssum]:
    5.44    "\<lbrakk>P \<bottom>;
    5.45     \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
    5.46     \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
    5.47 @@ -203,7 +203,7 @@
    5.48  
    5.49  subsection {* Strict sum preserves flatness *}
    5.50  
    5.51 -instance "++" :: (flat, flat) flat
    5.52 +instance ssum :: (flat, flat) flat
    5.53  apply (intro_classes, clarify)
    5.54  apply (case_tac x, simp)
    5.55  apply (case_tac y, simp_all add: flat_below_iff)
    5.56 @@ -296,7 +296,7 @@
    5.57  
    5.58  subsection {* Strict sum is a bifinite domain *}
    5.59  
    5.60 -instantiation "++" :: (bifinite, bifinite) bifinite
    5.61 +instantiation ssum :: (bifinite, bifinite) bifinite
    5.62  begin
    5.63  
    5.64  definition
     6.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 17:20:03 2010 -0800
     6.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 17:21:10 2010 -0800
     6.3 @@ -31,9 +31,9 @@
     6.4  
     6.5  (* FIXME: use theory data for this *)
     6.6  val copy_tab : string Symtab.table =
     6.7 -    Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
     6.8 -                 (@{type_name "++"}, @{const_name "ssum_map"}),
     6.9 -                 (@{type_name "**"}, @{const_name "sprod_map"}),
    6.10 +    Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
    6.11 +                 (@{type_name ssum}, @{const_name "ssum_map"}),
    6.12 +                 (@{type_name sprod}, @{const_name "sprod_map"}),
    6.13                   (@{type_name "*"}, @{const_name "cprod_map"}),
    6.14                   (@{type_name "u"}, @{const_name "u_map"})];
    6.15  
     7.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 17:20:03 2010 -0800
     7.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 17:21:10 2010 -0800
     7.3 @@ -79,7 +79,9 @@
     7.4            | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
     7.5            | rm_sorts (TVar(s,_))  = TVar(s,[])
     7.6          and remove_sorts l = map rm_sorts l;
     7.7 -        val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
     7.8 +        val indirect_ok =
     7.9 +            [@{type_name "*"}, @{type_name cfun}, @{type_name ssum},
    7.10 +             @{type_name sprod}, @{type_name u}];
    7.11          fun analyse indirect (TFree(v,s))  =
    7.12              (case AList.lookup (op =) tvars v of 
    7.13                 NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
     8.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 17:20:03 2010 -0800
     8.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 17:21:10 2010 -0800
     8.3 @@ -213,8 +213,8 @@
     8.4  (* ----- combinators for making dtyps ----- *)
     8.5  
     8.6  fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
     8.7 -fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name "**"}, [T, U]);
     8.8 -fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name "++"}, [T, U]);
     8.9 +fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]);
    8.10 +fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]);
    8.11  fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
    8.12  val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
    8.13  val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
    8.14 @@ -231,9 +231,9 @@
    8.15  (* ----- support for type and mixfix expressions ----- *)
    8.16  
    8.17  fun mk_uT T = Type(@{type_name "u"}, [T]);
    8.18 -fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    8.19 -fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
    8.20 -fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
    8.21 +fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
    8.22 +fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
    8.23 +fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
    8.24  val oneT = @{typ one};
    8.25  
    8.26  val op ->> = mk_cfunT;
     9.1 --- a/src/HOLCF/Tools/cont_consts.ML	Tue Mar 02 17:20:03 2010 -0800
     9.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Tue Mar 02 17:21:10 2010 -0800
     9.3 @@ -56,7 +56,7 @@
     9.4        trans_rules (syntax c2) (syntax c1) n mx)
     9.5    end;
     9.6  
     9.7 -fun cfun_arity (Type (n, [_, T])) = if n = @{type_name "->"} then 1 + cfun_arity T else 0
     9.8 +fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
     9.9    | cfun_arity _ = 0;
    9.10  
    9.11  fun is_contconst (_, _, NoSyn) = false
    10.1 --- a/src/HOLCF/Tools/fixrec.ML	Tue Mar 02 17:20:03 2010 -0800
    10.2 +++ b/src/HOLCF/Tools/fixrec.ML	Tue Mar 02 17:21:10 2010 -0800
    10.3 @@ -35,11 +35,11 @@
    10.4  (*************************************************************************)
    10.5  
    10.6  (* ->> is taken from holcf_logic.ML *)
    10.7 -fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    10.8 +fun cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
    10.9  
   10.10  infixr 6 ->>; val (op ->>) = cfunT;
   10.11  
   10.12 -fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
   10.13 +fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
   10.14    | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
   10.15  
   10.16  fun maybeT T = Type(@{type_name "maybe"}, [T]);
   10.17 @@ -53,11 +53,11 @@
   10.18  
   10.19  local
   10.20  
   10.21 -fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
   10.22 +fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
   10.23    | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
   10.24    | binder_cfun _   =  [];
   10.25  
   10.26 -fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
   10.27 +fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
   10.28    | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
   10.29    | body_cfun T   =  T;
   10.30  
   10.31 @@ -99,7 +99,7 @@
   10.32  fun mk_capply (t, u) =
   10.33    let val (S, T) =
   10.34      case Term.fastype_of t of
   10.35 -        Type(@{type_name "->"}, [S, T]) => (S, T)
   10.36 +        Type(@{type_name cfun}, [S, T]) => (S, T)
   10.37        | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
   10.38    in capply_const (S, T) $ t $ u end;
   10.39  
   10.40 @@ -288,7 +288,7 @@
   10.41    | Const(c,T) =>
   10.42        let
   10.43          val n = Name.variant taken "v";
   10.44 -        fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
   10.45 +        fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
   10.46            | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
   10.47            | result_type T _ = T;
   10.48          val v = Free(n, result_type T vs);
    11.1 --- a/src/HOLCF/Tools/holcf_library.ML	Tue Mar 02 17:20:03 2010 -0800
    11.2 +++ b/src/HOLCF/Tools/holcf_library.ML	Tue Mar 02 17:21:10 2010 -0800
    11.3 @@ -51,12 +51,12 @@
    11.4  (*** Continuous function space ***)
    11.5  
    11.6  (* ->> is taken from holcf_logic.ML *)
    11.7 -fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    11.8 +fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
    11.9  
   11.10  val (op ->>) = mk_cfunT;
   11.11  val (op -->>) = Library.foldr mk_cfunT;
   11.12  
   11.13 -fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
   11.14 +fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
   11.15    | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
   11.16  
   11.17  fun capply_const (S, T) =
   11.18 @@ -84,7 +84,7 @@
   11.19  fun mk_capply (t, u) =
   11.20    let val (S, T) =
   11.21      case fastype_of t of
   11.22 -        Type(@{type_name "->"}, [S, T]) => (S, T)
   11.23 +        Type(@{type_name cfun}, [S, T]) => (S, T)
   11.24        | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
   11.25    in capply_const (S, T) $ t $ u end;
   11.26  
   11.27 @@ -153,9 +153,9 @@
   11.28  
   11.29  val oneT = @{typ "one"};
   11.30  
   11.31 -fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
   11.32 +fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
   11.33  
   11.34 -fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U)
   11.35 +fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U)
   11.36    | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
   11.37  
   11.38  fun spair_const (T, U) =
   11.39 @@ -179,9 +179,9 @@
   11.40  
   11.41  (*** Strict sum type ***)
   11.42  
   11.43 -fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
   11.44 +fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
   11.45  
   11.46 -fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U)
   11.47 +fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U)
   11.48    | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []);
   11.49  
   11.50  fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U));
    12.1 --- a/src/HOLCF/Tools/repdef.ML	Tue Mar 02 17:20:03 2010 -0800
    12.2 +++ b/src/HOLCF/Tools/repdef.ML	Tue Mar 02 17:21:10 2010 -0800
    12.3 @@ -35,7 +35,7 @@
    12.4  val natT = @{typ nat};
    12.5  val udomT = @{typ udom};
    12.6  fun alg_deflT T = Type (@{type_name alg_defl}, [T]);
    12.7 -fun cfunT (T, U) = Type (@{type_name "->"}, [T, U]);
    12.8 +fun cfunT (T, U) = Type (@{type_name cfun}, [T, U]);
    12.9  fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT));
   12.10  fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T));
   12.11  fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T));