# HG changeset patch
# User wenzelm
# Date 1632081311 -7200
# Node ID 714e87ce6e9d30094b17782569f9b90bb0337a88
# Parent  dd04da556d1a57725821fce37d8360422b0f9f31
clarified signature;
clarified antiquotations;

diff -r dd04da556d1a -r 714e87ce6e9d src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Sun Sep 19 21:47:10 2021 +0200
+++ b/src/FOL/fologic.ML	Sun Sep 19 21:55:11 2021 +0200
@@ -15,8 +15,8 @@
   val dest_conj: term -> term list
   val mk_iff: term * term -> term
   val dest_iff: term -> term * term
-  val mk_all: term * term -> term
-  val mk_exists: term * term -> term
+  val mk_all: string * typ -> term -> term
+  val mk_exists: string * typ -> term -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
 end;
@@ -46,7 +46,7 @@
 
 val dest_eq = \<^Const_fn>\<open>eq _ for lhs rhs => \<open>(lhs, rhs)\<close>\<close>;
 
-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>;
+fun mk_all (x, T) P = \<^Const>\<open>All T for \<open>absfree (x, T) P\<close>\<close>;
+fun mk_exists (x, T) P = \<^Const>\<open>Ex T for \<open>absfree (x, T) P\<close>\<close>;
 
 end;
diff -r dd04da556d1a -r 714e87ce6e9d src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sun Sep 19 21:47:10 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Sun Sep 19 21:55:11 2021 +0200
@@ -109,8 +109,9 @@
         val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
         val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
         val zeq = FOLogic.mk_eq (Free(z', \<^Type>\<open>i\<close>), #1 (Ind_Syntax.rule_concl intr))
-    in List.foldr FOLogic.mk_exists
-             (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
+    in
+      fold_rev (FOLogic.mk_exists o Term.dest_Free) exfrees
+        (Balanced_Tree.make FOLogic.mk_conj (zeq::prems))
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
@@ -389,9 +390,8 @@
            val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
                             elem_factors ---> \<^Type>\<open>o\<close>)
            val qconcl =
-             List.foldr FOLogic.mk_all
-               (\<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
-                      $ (list_comb (pfree, elem_frees))) elem_frees
+             fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
+               \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
        in  (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
             qconcl)
        end;
@@ -400,7 +400,7 @@
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
-         \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
+         \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>;
 
      (*To instantiate the main induction rule*)
      val induct_concl =