# HG changeset patch
# User wenzelm
# Date 1727019628 -7200
# Node ID 6c1146e6e79eb303c2b586feb56d9ba15db19021
# Parent  92d2ceda2370bf1e5b65a43f5c7994073065d5dc
more antiquotations;

diff -r 92d2ceda2370 -r 6c1146e6e79e src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 22 16:18:49 2024 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 22 17:40:28 2024 +0200
@@ -391,12 +391,14 @@
   let
     val Globals {h, domT, ranT, x, ...} = globals
 
-    (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
-    val ihyp = Logic.all_const domT $ Abs ("z", domT,
-      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
-        HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Ex1\<close>, (ranT --> boolT) --> boolT) $
-          Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
-      |> Thm.cterm_of ctxt
+    val ihyp =
+      \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt domT\<close>
+        and 'b = \<open>Thm.ctyp_of ctxt ranT\<close>
+        and 'c = \<open>Thm.ctyp_of ctxt (fastype_of x)\<close>
+        and x = \<open>Thm.cterm_of ctxt x\<close>
+        and R = \<open>Thm.cterm_of ctxt R\<close>
+        and G = \<open>Thm.cterm_of ctxt G\<close>
+        in cprop \<open>\<And>z::'a. R z x \<Longrightarrow> \<exists>!y::'b. G z y\<close> for x :: 'c\<close>
 
     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
@@ -494,8 +496,8 @@
       Thm.make_def_binding (Config.get lthy function_internals)
         (derived_name_suffix defname "_sumC")
     val f_def =
-      Abs ("x", domT, Const (\<^const_name>\<open>Fun_Def.THE_default\<close>, ranT --> (ranT --> boolT) --> ranT)
-        $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
+      \<^instantiate>\<open>'a = domT and 'b = ranT and d = default and G
+        in term \<open>\<lambda>x::'a. THE_default (d x) (\<lambda>y::'b. G x y)\<close>\<close>
       |> Syntax.check_term lthy
   in
     lthy |> Local_Theory.define
@@ -777,12 +779,11 @@
     val R' = Free (Rn, fastype_of R)
 
     val Rrel = Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
-    val inrel_R = Const (\<^const_name>\<open>Fun_Def.in_rel\<close>,
-      HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
+    val inrel_R = \<^Const>\<open>in_rel domT domT for Rrel\<close>
 
-    val wfR' = HOLogic.mk_Trueprop (Const (\<^const_abbrev>\<open>Wellfounded.wfP\<close>,
-      (domT --> domT --> boolT) --> boolT) $ R')
-      |> Thm.cterm_of ctxt' (* "wf R'" *)
+    val wfR' =
+      \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt' domT\<close>
+        and R = \<open>Thm.cterm_of ctxt' R'\<close> in cprop \<open>wfP R\<close>\<close>
 
     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
     val ihyp = Logic.all_const domT $ Abs ("z", domT,