--- 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;
--- 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;