# HG changeset patch
# User wenzelm
# Date 1632080830 -7200
# Node ID dd04da556d1a57725821fce37d8360422b0f9f31
# Parent  54b2e5f771daf27f1c23c3986b60cd8347e8add6
clarified antiquotations;

diff -r 54b2e5f771da -r dd04da556d1a src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Sun Sep 19 21:37:14 2021 +0200
+++ b/src/FOL/fologic.ML	Sun Sep 19 21:47:10 2021 +0200
@@ -15,16 +15,12 @@
   val dest_conj: term -> term list
   val mk_iff: term * term -> term
   val dest_iff: term -> term * term
-  val all_const: typ -> term
   val mk_all: term * term -> term
-  val exists_const: typ -> term
   val mk_exists: term * term -> term
-  val eq_const: typ -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
 end;
 
-
 structure FOLogic: FOLOGIC =
 struct
 
@@ -44,15 +40,13 @@
 
 val dest_iff = \<^Const_fn>\<open>iff for A B => \<open>(A, B)\<close>\<close>;
 
-fun eq_const T = \<^Const>\<open>eq T\<close>;
-fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
+fun mk_eq (t, u) =
+  let val T = fastype_of t
+  in \<^Const>\<open>eq T for t u\<close> end;
 
 val dest_eq = \<^Const_fn>\<open>eq _ for lhs rhs => \<open>(lhs, rhs)\<close>\<close>;
 
-fun all_const T = \<^Const>\<open>All T\<close>;
-fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
-
-fun exists_const T = \<^Const>\<open>Ex T\<close>;
-fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
+fun mk_all (Free (x, T), P) = \<^Const>\<open>All T for \<open>absfree (x, T) P\<close>\<close>;
+fun mk_exists (Free (x, T), P) = \<^Const>\<open>Ex T for \<open>absfree (x, T) P\<close>\<close>;
 
 end;
diff -r 54b2e5f771da -r dd04da556d1a src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sun Sep 19 21:37:14 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Sun Sep 19 21:47:10 2021 +0200
@@ -20,8 +20,10 @@
 
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
-    FOLogic.all_const \<^Type>\<open>i\<close> $
-      Abs("v", \<^Type>\<open>i\<close>, \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
+  let val T = \<^Type>\<open>i\<close> in
+    \<^Const>\<open>All T for
+      \<open>Abs ("v", T, \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> A\<close>\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
+  end;
 
 fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;