# HG changeset patch
# User wenzelm
# Date 1631478711 -7200
# Node ID 28a582aa25ddb0464817e71f9a9469948ba94a57
# Parent  1466f8a2f6dd3d271521e18b213b2a85553bde48
more antiquotations;

diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy	Sun Sep 12 22:31:51 2021 +0200
@@ -156,7 +156,7 @@
 translations "UU" \<rightharpoonup> "CONST bottom"
 
 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
-setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close>
+setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
 
 text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -75,7 +75,7 @@
     (thy : theory)
     : thm * theory =
   let
-    val i = Free ("i", natT)
+    val i = Free ("i", \<^Type>\<open>nat\<close>)
     val T = (fst o dest_cfunT o range_type o fastype_of) take_const
 
     val lub_take_eqn =
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -42,13 +42,13 @@
   val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy
 
   val n = Free ("n", \<^typ>\<open>nat\<close>)
-  val n' = \<^const>\<open>Suc\<close> $ n
+  val n' = \<^Const>\<open>Suc for n\<close>
 
   local
     val newTs = map (#absT o #iso_info) constr_infos
     val subs = newTs ~~ map (fn t => t $ n) take_consts
-    fun is_ID (Const (c, _)) = (c = \<^const_name>\<open>ID\<close>)
-      | is_ID _              = false
+    fun is_ID \<^Const_>\<open>ID _\<close> = true
+      | is_ID _ = false
   in
     fun map_of_arg thy v T =
       let val m = Domain_Take_Proofs.map_of_typ thy subs T
@@ -110,10 +110,10 @@
   val newTs = map #absT iso_infos
   val P_names = Old_Datatype_Prop.indexify_names (map (K "P") newTs)
   val x_names = Old_Datatype_Prop.indexify_names (map (K "x") newTs)
-  val P_types = map (fn T => T --> HOLogic.boolT) newTs
+  val P_types = map (fn T => T --> \<^Type>\<open>bool\<close>) newTs
   val Ps = map Free (P_names ~~ P_types)
   val xs = map Free (x_names ~~ newTs)
-  val n = Free ("n", HOLogic.natT)
+  val n = Free ("n", \<^Type>\<open>nat\<close>)
 
   fun con_assm defined p (con, args) =
     let
@@ -257,14 +257,14 @@
   val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info
 
   val R_names = Old_Datatype_Prop.indexify_names (map (K "R") newTs)
-  val R_types = map (fn T => T --> T --> boolT) newTs
+  val R_types = map (fn T => T --> T --> \<^Type>\<open>bool\<close>) newTs
   val Rs = map Free (R_names ~~ R_types)
-  val n = Free ("n", natT)
+  val n = Free ("n", \<^Type>\<open>nat\<close>)
   val reserved = "x" :: "y" :: R_names
 
   (* declare bisimulation predicate *)
   val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
-  val bisim_type = R_types ---> boolT
+  val bisim_type = R_types ---> \<^Type>\<open>bool\<close>
   val (bisim_const, thy) =
       Sign.declare_const_global ((bisim_bind, bisim_type), NoSyn) thy
 
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -53,32 +53,29 @@
 val deflT = \<^typ>\<open>udom defl\<close>
 val udeflT = \<^typ>\<open>udom u defl\<close>
 
-fun mk_DEFL T =
-  Const (\<^const_name>\<open>defl\<close>, Term.itselfT T --> deflT) $ Logic.mk_type T
+fun mk_DEFL T = \<^Const>\<open>defl T for \<open>Logic.mk_type T\<close>\<close>
 
-fun dest_DEFL (Const (\<^const_name>\<open>defl\<close>, _) $ t) = Logic.dest_type t
+fun dest_DEFL \<^Const_>\<open>defl _ for t\<close> = Logic.dest_type t
   | dest_DEFL t = raise TERM ("dest_DEFL", [t])
 
-fun mk_LIFTDEFL T =
-  Const (\<^const_name>\<open>liftdefl\<close>, Term.itselfT T --> udeflT) $ Logic.mk_type T
+fun mk_LIFTDEFL T = \<^Const>\<open>liftdefl T for \<open>Logic.mk_type T\<close>\<close>
 
-fun dest_LIFTDEFL (Const (\<^const_name>\<open>liftdefl\<close>, _) $ t) = Logic.dest_type t
+fun dest_LIFTDEFL \<^Const_>\<open>liftdefl _ for t\<close> = Logic.dest_type t
   | dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t])
 
-fun mk_u_defl t = mk_capply (\<^const>\<open>u_defl\<close>, t)
+fun mk_u_defl t = mk_capply (\<^Const>\<open>u_defl\<close>, t)
 
-fun emb_const T = Const (\<^const_name>\<open>emb\<close>, T ->> udomT)
-fun prj_const T = Const (\<^const_name>\<open>prj\<close>, udomT ->> T)
+fun emb_const T = \<^Const>\<open>emb T\<close>
+fun prj_const T = \<^Const>\<open>prj T\<close>
 fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
 
-fun isodefl_const T =
-  Const (\<^const_name>\<open>isodefl\<close>, (T ->> T) --> deflT --> HOLogic.boolT)
+fun isodefl_const T = \<^Const>\<open>isodefl T\<close>
 
-fun isodefl'_const T =
-  Const (\<^const_name>\<open>isodefl'\<close>, (T ->> T) --> udeflT --> HOLogic.boolT)
+fun isodefl'_const T = \<^Const>\<open>isodefl' T\<close>
 
 fun mk_deflation t =
-  Const (\<^const_name>\<open>deflation\<close>, Term.fastype_of t --> boolT) $ t
+  let val T = #1 (dest_cfunT (Term.fastype_of t))
+  in \<^Const>\<open>deflation T for t\<close> end
 
 (* splits a cterm into the right and lefthand sides of equality *)
 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
@@ -121,10 +118,10 @@
     (* convert parameters to lambda abstractions *)
     fun mk_eqn (lhs, rhs) =
         case lhs of
-          Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ (x as Free _) =>
+          \<^Const_>\<open>Rep_cfun _ _ for f \<open>x as Free _\<close>\<close> =>
             mk_eqn (f, big_lambda x rhs)
-        | f $ Const (\<^const_name>\<open>Pure.type\<close>, T) =>
-            mk_eqn (f, Abs ("t", T, rhs))
+        | f $ \<^Const_>\<open>Pure.type T\<close> =>
+            mk_eqn (f, Abs ("t", \<^Type>\<open>itself T\<close>, rhs))
         | Const _ => Logic.mk_equals (lhs, rhs)
         | _ => raise TERM ("lhs not of correct form", [lhs, rhs])
     val eqns = map mk_eqn projs
@@ -710,7 +707,7 @@
     (* prove lub of take equals ID *)
     fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
       let
-        val n = Free ("n", natT)
+        val n = Free ("n", \<^Type>\<open>nat\<close>)
         val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
         fun tac ctxt =
             EVERY
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -149,7 +149,8 @@
 infix 9 `
 
 fun mk_deflation t =
-  Const (\<^const_name>\<open>deflation\<close>, Term.fastype_of t --> boolT) $ t
+  let val T = #1 (dest_cfunT (Term.fastype_of t))
+  in \<^Const>\<open>deflation T for t\<close> end
 
 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
 
@@ -235,7 +236,7 @@
           (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)))
     val take_rhss =
       let
-        val n = Free ("n", HOLogic.natT)
+        val n = Free ("n", \<^Type>\<open>nat\<close>)
         val rhs = mk_iterate (n, take_functional)
       in
         map (lambda n o snd) (mk_projs dbinds rhs)
@@ -244,7 +245,7 @@
     (* define take constants *)
     fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
       let
-        val take_type = HOLogic.natT --> lhsT ->> lhsT
+        val take_type = \<^Type>\<open>nat\<close> --> lhsT ->> lhsT
         val take_bind = Binding.suffix_name "_take" dbind
         val (take_const, thy) =
           Sign.declare_const_global ((take_bind, take_type), NoSyn) thy
@@ -284,7 +285,7 @@
       fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy
 
     (* prove take_Suc lemmas *)
-    val n = Free ("n", natT)
+    val n = Free ("n", \<^Type>\<open>nat\<close>)
     val take_is = map (fn t => t $ n) take_consts
     fun prove_take_Suc
           (((take_const, rep_abs), dbind), (_, rhsT)) thy =
@@ -308,7 +309,7 @@
     val deflation_abs_rep_thms = map deflation_abs_rep iso_infos
     val deflation_take_thm =
       let
-        val n = Free ("n", natT)
+        val n = Free ("n", \<^Type>\<open>nat\<close>)
         fun mk_goal take_const = mk_deflation (take_const $ n)
         val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
         val bottom_rules =
@@ -380,14 +381,14 @@
     (* define finiteness predicates *)
     fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
       let
-        val finite_type = lhsT --> boolT
+        val finite_type = lhsT --> \<^Type>\<open>bool\<close>
         val finite_bind = Binding.suffix_name "_finite" dbind
         val (finite_const, thy) =
           Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy
         val x = Free ("x", lhsT)
-        val n = Free ("n", natT)
+        val n = Free ("n", \<^Type>\<open>nat\<close>)
         val finite_rhs =
-          lambda x (HOLogic.exists_const natT $
+          lambda x (HOLogic.exists_const \<^Type>\<open>nat\<close> $
             (lambda n (mk_eq (mk_capply (take_const $ n, x), x))))
         val finite_eqn = Logic.mk_equals (finite_const, finite_rhs)
         val (finite_def_thm, thy) =
@@ -436,7 +437,8 @@
             map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms
         val n = Free ("n", \<^typ>\<open>nat\<close>)
         fun mk_decisive t =
-            Const (\<^const_name>\<open>decisive\<close>, fastype_of t --> boolT) $ t
+          let val T = #1 (dest_cfunT (fastype_of t))
+          in \<^Const>\<open>decisive T for t\<close> end
         fun f take_const = mk_decisive (take_const $ n)
         val goal = mk_trp (foldr1 mk_conj (map f take_consts))
         val rules0 = @{thm decisive_bottom} :: take_0_thms
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/cont_consts.ML
--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -18,7 +18,7 @@
 (* misc utils *)
 
 fun change_arrow 0 T = T
-  | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T])
+  | change_arrow n (Type (_, [S, T])) = \<^Type>\<open>fun S \<open>change_arrow (n - 1) T\<close>\<close>
   | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
 
 fun trans_rules name2 name1 n mx =
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -24,12 +24,9 @@
 val cont_R = @{thm cont_Rep_cfun2}
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ t $ u) =
-      is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ Abs (_, _, t)) =
-      is_lcf_term t
-  | is_lcf_term (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ t) =
-      is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
+fun is_lcf_term \<^Const_>\<open>Rep_cfun _ _ for t u\<close> = is_lcf_term t andalso is_lcf_term u
+  | is_lcf_term \<^Const_>\<open>Abs_cfun _ _ for \<open>Abs (_, _, t)\<close>\<close> = is_lcf_term t
+  | is_lcf_term \<^Const_>\<open>Abs_cfun _ _ for t\<close> = is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = not (Term.is_open t)
 
@@ -64,17 +61,17 @@
   (* 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 (\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ t) =
+  fun cont_thms1 b \<^Const_>\<open>Rep_cfun _ _ for f t\<close> =
     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 (\<^const_name>\<open>Abs_cfun\<close>, _) $ Abs (_, _, t)) =
+    | cont_thms1 b \<^Const_>\<open>Abs_cfun _ _ for \<open>Abs (_, _, t)\<close>\<close> =
     let
       val (cs, ls) = cont_thms1 b t
       val (cs', l) = lam cs
     in (cs', l::ls) end
-    | cont_thms1 b (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ t) =
+    | cont_thms1 b \<^Const_>\<open>Abs_cfun _ _ for t\<close> =
     let
       val t' = Term.incr_boundvars 1 t $ Bound 0
       val (cs, ls) = cont_thms1 b t'
@@ -104,9 +101,9 @@
         [] => no_tac
       | (c::_) => resolve_tac ctxt [c] i
 
-    fun cont_tac_of_term (Const (\<^const_name>\<open>cont\<close>, _) $ f) =
+    fun cont_tac_of_term \<^Const_>\<open>cont _ _ for f\<close> =
       let
-        val f' = Const (\<^const_name>\<open>Abs_cfun\<close>, dummyT) $ f
+        val f' = \<^Const>\<open>Abs_cfun dummyT dummyT for f\<close>
       in
         if is_lcf_term f'
         then new_cont_tac f'
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -53,10 +53,10 @@
 
 (* building terms *)
 
-fun adm_const T = Const (\<^const_name>\<open>adm\<close>, (T --> HOLogic.boolT) --> HOLogic.boolT)
+fun adm_const T = \<^Const>\<open>adm T\<close>
 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P
 
-fun below_const T = Const (\<^const_name>\<open>below\<close>, T --> T --> HOLogic.boolT)
+fun below_const T = \<^Const>\<open>below T\<close>
 
 (* proving class instances *)
 
@@ -229,7 +229,7 @@
     val (newT, oldT, set) = prepare prep_term name typ raw_set thy
 
     val goal_bottom_mem =
-      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (\<^const_name>\<open>bottom\<close>, oldT), set))
+      HOLogic.mk_Trueprop (HOLogic.mk_mem (\<^Const>\<open>bottom oldT\<close>, set))
 
     val goal_admissible =
       HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -50,19 +50,17 @@
 
 val udomT = \<^typ>\<open>udom\<close>
 val deflT = \<^typ>\<open>udom defl\<close>
-val udeflT = \<^typ>\<open>udom u defl\<close>
-fun emb_const T = Const (\<^const_name>\<open>emb\<close>, T ->> udomT)
-fun prj_const T = Const (\<^const_name>\<open>prj\<close>, udomT ->> T)
-fun defl_const T = Const (\<^const_name>\<open>defl\<close>, Term.itselfT T --> deflT)
-fun liftemb_const T = Const (\<^const_name>\<open>liftemb\<close>, mk_upT T ->> mk_upT udomT)
-fun liftprj_const T = Const (\<^const_name>\<open>liftprj\<close>, mk_upT udomT ->> mk_upT T)
-fun liftdefl_const T = Const (\<^const_name>\<open>liftdefl\<close>, Term.itselfT T --> udeflT)
+fun emb_const T = \<^Const>\<open>emb T\<close>
+fun prj_const T = \<^Const>\<open>prj T\<close>
+fun defl_const T = \<^Const>\<open>defl T\<close>
+fun liftemb_const T = \<^Const>\<open>liftemb T\<close>
+fun liftprj_const T = \<^Const>\<open>liftprj T\<close>
+fun liftdefl_const T = \<^Const>\<open>liftdefl T\<close>
 
 fun mk_u_map t =
   let
     val (T, U) = dest_cfunT (fastype_of t)
-    val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
-    val u_map_const = Const (\<^const_name>\<open>u_map\<close>, u_map_type)
+    val u_map_const = \<^Const>\<open>u_map T U\<close>
   in
     mk_capply (u_map_const, t)
   end
@@ -124,7 +122,7 @@
     val liftdefl_eqn =
       Logic.mk_equals (liftdefl_const newT,
         Abs ("t", Term.itselfT newT,
-          mk_capply (\<^const>\<open>liftdefl_of\<close>, defl_const newT $ Logic.mk_type newT)))
+          mk_capply (\<^Const>\<open>liftdefl_of\<close>, defl_const newT $ Logic.mk_type newT)))
 
     val name_def = Thm.def_binding tname
     val emb_bind = (Binding.prefix_name "emb_" name_def, [])
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -34,12 +34,12 @@
 
 local
 
-fun binder_cfun (Type(\<^type_name>\<open>cfun\<close>,[T, U])) = T :: binder_cfun U
-  | binder_cfun (Type(\<^type_name>\<open>fun\<close>,[T, U])) = T :: binder_cfun U
+fun binder_cfun \<^Type>\<open>cfun T U\<close> = T :: binder_cfun U
+  | binder_cfun \<^Type>\<open>fun T U\<close> = T :: binder_cfun U
   | binder_cfun _   =  []
 
-fun body_cfun (Type(\<^type_name>\<open>cfun\<close>,[_, U])) = body_cfun U
-  | body_cfun (Type(\<^type_name>\<open>fun\<close>,[_, U])) = body_cfun U
+fun body_cfun \<^Type>\<open>cfun _ U\<close> = body_cfun U
+  | body_cfun \<^Type>\<open>fun _ U\<close> = body_cfun U
   | body_cfun T   =  T
 
 in
@@ -59,24 +59,23 @@
 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
 
 (* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(\<^const_name>\<open>Rep_cfun\<close>,_)$f$_) = chead_of f
+fun chead_of \<^Const_>\<open>Rep_cfun _ _ for f _\<close> = chead_of f
   | chead_of u = u
 
 infix 1 === val (op ===) = HOLogic.mk_eq
 
 fun mk_mplus (t, u) =
-  let val mT = Term.fastype_of t
-  in Const(\<^const_name>\<open>Fixrec.mplus\<close>, mT ->> mT ->> mT) ` t ` u end
+  let val T = dest_matchT (Term.fastype_of t)
+  in \<^Const>\<open>Fixrec.mplus T\<close> ` t ` u end
 
 fun mk_run t =
   let
     val mT = Term.fastype_of t
     val T = dest_matchT mT
-    val run = Const(\<^const_name>\<open>Fixrec.run\<close>, mT ->> T)
+    val run = \<^Const>\<open>Fixrec.run T\<close>
   in
     case t of
-      Const(\<^const_name>\<open>Rep_cfun\<close>, _) $
-        Const(\<^const_name>\<open>Fixrec.succeed\<close>, _) $ u => u
+      \<^Const_>\<open>Rep_cfun _ _\<close> $ \<^Const_>\<open>Fixrec.succeed _\<close> $ u => u
     | _ => run ` t
   end
 
@@ -150,7 +149,7 @@
       |> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs)
     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]
     val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms)
-    val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT)
+    val P = Var (("P", 0), map Term.fastype_of lhss ---> \<^Type>\<open>bool\<close>)
     val predicate = lambda_tuple lhss (list_comb (P, lhss))
     val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
       |> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
@@ -219,7 +218,7 @@
     (* compiles a monadic term for a constructor pattern *)
     and comp_con T p rhs vs taken =
       case p of
-        Const(\<^const_name>\<open>Rep_cfun\<close>,_) $ f $ x =>
+        \<^Const_>\<open>Rep_cfun _ _ for f x\<close> =>
           let val (rhs', v, taken') = comp_pat x rhs taken
           in comp_con T f rhs' (v::vs) taken' end
       | f $ x =>
@@ -243,7 +242,7 @@
 (* returns (constant, (vars, matcher)) *)
 fun compile_lhs match_name pat rhs vs taken =
   case pat of
-    Const(\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ x =>
+    \<^Const_>\<open>Rep_cfun _ _ for f x\<close> =>
       let val (rhs', v, taken') = compile_pat match_name x rhs taken
       in compile_lhs match_name f rhs' (v::vs) taken' end
   | Free(_,_) => (pat, (vs, rhs))
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -13,10 +13,6 @@
 
 (*** Operations from Isabelle/HOL ***)
 
-val boolT = HOLogic.boolT
-val natT = HOLogic.natT
-val mk_setT = HOLogic.mk_setT
-
 val mk_equals = Logic.mk_equals
 val mk_eq = HOLogic.mk_eq
 val mk_trp = HOLogic.mk_Trueprop
@@ -33,9 +29,9 @@
 
 (*** Basic HOLCF concepts ***)
 
-fun mk_bottom T = Const (\<^const_name>\<open>bottom\<close>, T)
+fun mk_bottom T = \<^Const>\<open>bottom T\<close>
 
-fun below_const T = Const (\<^const_name>\<open>below\<close>, [T, T] ---> boolT)
+fun below_const T = \<^Const>\<open>below T\<close>
 fun mk_below (t, u) = below_const (fastype_of t) $ t $ u
 
 fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t))
@@ -43,44 +39,40 @@
 fun mk_defined t = mk_not (mk_undef t)
 
 fun mk_adm t =
-  Const (\<^const_name>\<open>adm\<close>, fastype_of t --> boolT) $ t
+  let val T = Term.domain_type (fastype_of t)
+  in \<^Const>\<open>adm T for t\<close> end
 
 fun mk_compact t =
-  Const (\<^const_name>\<open>compact\<close>, fastype_of t --> boolT) $ t
+  let val T = fastype_of t
+  in \<^Const>\<open>compact T for t\<close> end
 
 fun mk_cont t =
-  Const (\<^const_name>\<open>cont\<close>, fastype_of t --> boolT) $ t
+  let val \<^Type>\<open>fun A B\<close> = fastype_of t
+  in \<^Const>\<open>cont A B for t\<close> end
 
 fun mk_chain t =
-  Const (\<^const_name>\<open>chain\<close>, Term.fastype_of t --> boolT) $ t
+  let val T = Term.range_type (Term.fastype_of t)
+  in \<^Const>\<open>chain T for t\<close> end
 
 fun mk_lub t =
   let
     val T = Term.range_type (Term.fastype_of t)
-    val lub_const = Const (\<^const_name>\<open>lub\<close>, mk_setT T --> T)
     val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
-    val image_type = (natT --> T) --> mk_setT natT --> mk_setT T
-    val image_const = Const (\<^const_name>\<open>image\<close>, image_type)
-  in
-    lub_const $ (image_const $ t $ UNIV_const)
-  end
+  in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end
 
 
 (*** Continuous function space ***)
 
-fun mk_cfunT (T, U) = Type(\<^type_name>\<open>cfun\<close>, [T, U])
+fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close>
 
 val (op ->>) = mk_cfunT
 val (op -->>) = Library.foldr mk_cfunT
 
-fun dest_cfunT (Type(\<^type_name>\<open>cfun\<close>, [T, U])) = (T, U)
+fun dest_cfunT \<^Type>\<open>cfun T U\<close> = (T, U)
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], [])
 
-fun capply_const (S, T) =
-  Const(\<^const_name>\<open>Rep_cfun\<close>, (S ->> T) --> (S --> T))
-
-fun cabs_const (S, T) =
-  Const(\<^const_name>\<open>Abs_cfun\<close>, (S --> T) --> (S ->> T))
+fun capply_const (S, T) = \<^Const>\<open>Rep_cfun S T\<close>
+fun cabs_const (S, T) = \<^Const>\<open>Abs_cfun S T\<close>
 
 fun mk_cabs t =
   let val T = fastype_of t
@@ -101,7 +93,7 @@
 fun mk_capply (t, u) =
   let val (S, T) =
     case fastype_of t of
-        Type(\<^type_name>\<open>cfun\<close>, [S, T]) => (S, T)
+        \<^Type>\<open>cfun S T\<close> => (S, T)
       | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u])
   in capply_const (S, T) $ t $ u end
 
@@ -109,10 +101,7 @@
 
 val list_ccomb : term * term list -> term = Library.foldl mk_capply
 
-fun mk_ID T = Const (\<^const_name>\<open>ID\<close>, T ->> T)
-
-fun cfcomp_const (T, U, V) =
-  Const (\<^const_name>\<open>cfcomp\<close>, (U ->> V) ->> (T ->> U) ->> (T ->> V))
+fun mk_ID T = \<^Const>\<open>ID T\<close>
 
 fun mk_cfcomp (f, g) =
   let
@@ -120,12 +109,13 @@
     val (T, U') = dest_cfunT (fastype_of g)
   in
     if U = U'
-    then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
+    then mk_capply (mk_capply (\<^Const>\<open>cfcomp U V T\<close>, f), g)
     else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
   end
 
-fun strictify_const T = Const (\<^const_name>\<open>strictify\<close>, T ->> T)
-fun mk_strictify t = strictify_const (fastype_of t) ` t
+fun mk_strictify t =
+  let val (T, U) = dest_cfunT (fastype_of t)
+  in \<^Const>\<open>strictify T U\<close> ` t end;
 
 fun mk_strict t =
   let val (T, U) = dest_cfunT (fastype_of t)
@@ -154,17 +144,16 @@
 
 (*** Lifted cpo type ***)
 
-fun mk_upT T = Type(\<^type_name>\<open>u\<close>, [T])
+fun mk_upT T = \<^Type>\<open>u T\<close>
 
-fun dest_upT (Type(\<^type_name>\<open>u\<close>, [T])) = T
+fun dest_upT \<^Type>\<open>u T\<close> = T
   | dest_upT T = raise TYPE ("dest_upT", [T], [])
 
-fun up_const T = Const(\<^const_name>\<open>up\<close>, T ->> mk_upT T)
+fun up_const T = \<^Const>\<open>up T\<close>
 
 fun mk_up t = up_const (fastype_of t) ` t
 
-fun fup_const (T, U) =
-  Const(\<^const_name>\<open>fup\<close>, (T ->> U) ->> mk_upT T ->> U)
+fun fup_const (T, U) = \<^Const>\<open>fup T U\<close>
 
 fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t
 
@@ -175,19 +164,18 @@
 
 val oneT = \<^typ>\<open>one\<close>
 
-fun one_case_const T = Const (\<^const_name>\<open>one_case\<close>, T ->> oneT ->> T)
+fun one_case_const T = \<^Const>\<open>one_case T\<close>
 fun mk_one_case t = one_case_const (fastype_of t) ` t
 
 
 (*** Strict product type ***)
 
-fun mk_sprodT (T, U) = Type(\<^type_name>\<open>sprod\<close>, [T, U])
+fun mk_sprodT (T, U) = \<^Type>\<open>sprod T U\<close>
 
-fun dest_sprodT (Type(\<^type_name>\<open>sprod\<close>, [T, U])) = (T, U)
+fun dest_sprodT \<^Type>\<open>sprod T U\<close> = (T, U)
   | dest_sprodT T = raise TYPE ("dest_sprodT", [T], [])
 
-fun spair_const (T, U) =
-  Const(\<^const_name>\<open>spair\<close>, T ->> U ->> mk_sprodT (T, U))
+fun spair_const (T, U) = \<^Const>\<open>spair T U\<close>
 
 (* builds the expression (:t, u:) *)
 fun mk_spair (t, u) =
@@ -198,14 +186,11 @@
   | mk_stuple (t::[]) = t
   | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts)
 
-fun sfst_const (T, U) =
-  Const(\<^const_name>\<open>sfst\<close>, mk_sprodT (T, U) ->> T)
+fun sfst_const (T, U) = \<^Const>\<open>sfst T U\<close>
 
-fun ssnd_const (T, U) =
-  Const(\<^const_name>\<open>ssnd\<close>, mk_sprodT (T, U) ->> U)
+fun ssnd_const (T, U) = \<^Const>\<open>ssnd T U\<close>
 
-fun ssplit_const (T, U, V) =
-  Const (\<^const_name>\<open>ssplit\<close>, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V)
+fun ssplit_const (T, U, V) = \<^Const>\<open>ssplit T U V\<close>
 
 fun mk_ssplit t =
   let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t))
@@ -214,13 +199,13 @@
 
 (*** Strict sum type ***)
 
-fun mk_ssumT (T, U) = Type(\<^type_name>\<open>ssum\<close>, [T, U])
+fun mk_ssumT (T, U) = \<^Type>\<open>ssum T U\<close>
 
-fun dest_ssumT (Type(\<^type_name>\<open>ssum\<close>, [T, U])) = (T, U)
+fun dest_ssumT \<^Type>\<open>ssum T U\<close> = (T, U)
   | dest_ssumT T = raise TYPE ("dest_ssumT", [T], [])
 
-fun sinl_const (T, U) = Const(\<^const_name>\<open>sinl\<close>, T ->> mk_ssumT (T, U))
-fun sinr_const (T, U) = Const(\<^const_name>\<open>sinr\<close>, U ->> mk_ssumT (T, U))
+fun sinl_const (T, U) = \<^Const>\<open>sinl T U\<close>
+fun sinr_const (T, U) = \<^Const>\<open>sinr U T\<close>
 
 (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *)
 fun mk_sinjects ts =
@@ -240,9 +225,7 @@
     fst (inj (ts ~~ Ts))
   end
 
-fun sscase_const (T, U, V) =
-  Const(\<^const_name>\<open>sscase\<close>,
-    (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V)
+fun sscase_const (T, U, V) = \<^Const>\<open>sscase T V U\<close>
 
 fun mk_sscase (t, u) =
   let val (T, _) = dest_cfunT (fastype_of t)
@@ -258,14 +241,14 @@
 
 (*** pattern match monad type ***)
 
-fun mk_matchT T = Type (\<^type_name>\<open>match\<close>, [T])
+fun mk_matchT T = \<^Type>\<open>match T\<close>
 
-fun dest_matchT (Type(\<^type_name>\<open>match\<close>, [T])) = T
+fun dest_matchT \<^Type>\<open>match T\<close> = T
   | dest_matchT T = raise TYPE ("dest_matchT", [T], [])
 
-fun mk_fail T = Const (\<^const_name>\<open>Fixrec.fail\<close>, mk_matchT T)
+fun mk_fail T = \<^Const>\<open>Fixrec.fail T\<close>
 
-fun succeed_const T = Const (\<^const_name>\<open>Fixrec.succeed\<close>, T ->> mk_matchT T)
+fun succeed_const T = \<^Const>\<open>Fixrec.succeed T\<close>
 fun mk_succeed t = succeed_const (fastype_of t) ` t
 
 
@@ -278,10 +261,9 @@
 
 fun mk_fix t =
   let val (T, _) = dest_cfunT (fastype_of t)
-  in mk_capply (Const(\<^const_name>\<open>fix\<close>, (T ->> T) ->> T), t) end
+  in mk_capply (\<^Const>\<open>fix T\<close>, t) end
 
-fun iterate_const T =
-  Const (\<^const_name>\<open>iterate\<close>, natT --> (T ->> T) ->> (T ->> T))
+fun iterate_const T = \<^Const>\<open>iterate T\<close>
 
 fun mk_iterate (n, f) =
   let val (T, _) = dest_cfunT (Term.fastype_of f)
diff -r 1466f8a2f6dd -r 28a582aa25dd src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Sep 12 22:31:51 2021 +0200
@@ -457,11 +457,8 @@
       in
         pat_const $ p1 $ p2
       end;
-    fun mk_tuple_pat [] = succeed_const HOLogic.unitT
+    fun mk_tuple_pat [] = succeed_const \<^Type>\<open>unit\<close>
       | mk_tuple_pat ps = foldr1 mk_pair_pat ps;
-    fun branch_const (T,U,V) = 
-      Const (\<^const_name>\<open>branch\<close>,
-        (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
 
     (* define pattern combinators *)
     local
@@ -546,9 +543,9 @@
           val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
           val pats = map Free (patNs ~~ patTs);
           val k = Free ("rhs", mk_tupleT Vs ->> R);
-          val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
+          val branch1 = \<^Const>\<open>branch lhsT \<open>mk_tupleT Vs\<close> R\<close>;
           val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
-          val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
+          val branch2 = \<^Const>\<open>branch \<open>mk_tupleT Ts\<close> \<open>mk_tupleT Vs\<close> R\<close>;
           val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
           val taken = "rhs" :: patNs;
         in (fun1, fun2, taken) end;