diff --git a/src/FOL/fologic.ML b/src/FOL/fologic.ML
--- a/src/FOL/fologic.ML
+++ b/src/FOL/fologic.ML
@@ -1,58 +1,52 @@
 (*  Title:      FOL/fologic.ML
     Author:     Lawrence C Paulson
 
 Abstract syntax operations for FOL.
 *)
 
 signature FOLOGIC =
 sig
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
   val mk_conj: term * term -> term
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
   val dest_imp: term -> term * term
   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
 
 fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
 
 val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
 
 fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
 and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
 and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
 and mk_iff (t1, t2) = \<^Const>\<open>iff for t1 t2\<close>;
 
 val dest_imp = \<^Const_fn>\<open>imp for A B => \<open>(A, B)\<close>\<close>;
 
 fun dest_conj \<^Const_>\<open>conj for t t'\<close> = t :: dest_conj t'
   | dest_conj t = [t];
 
 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 --git a/src/ZF/ind_syntax.ML b/src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML
+++ b/src/ZF/ind_syntax.ML
@@ -1,117 +1,119 @@
 (*  Title:      ZF/ind_syntax.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Abstract Syntax functions for Inductive Definitions.
 *)
 
 structure Ind_Syntax =
 struct
 
 (*Print tracing messages during processing of "inductive" theory sections*)
 val trace = Unsynchronized.ref false;
 
 fun traceIt msg thy t =
   if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
   else t;
 
 
 (** Abstract syntax definitions for ZF **)
 
 (*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;
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
         error"Premises may not be conjuctive"
   | chk_prem rec_hd \<^Const_>\<open>mem for t X\<close> =
         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
   | chk_prem rec_hd t =
         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl =
     let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)
 fun rule_concl_msg sign rl = rule_concl rl
     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
                           Syntax.string_of_term_global sign rl);
 
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)
 val equals_CollectD =
     Rule_Insts.read_instantiate \<^context> [((("W", 0), Position.none), "Q")] ["Q"]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
 
 
 (** For datatype definitions **)
 
 (*Constructor name, type, mixfix info;
   internal name from mixfix, datatype sets, full premises*)
 type constructor_spec =
     (string * typ * mixfix) * string * term list * term list;
 
 fun dest_mem \<^Const_>\<open>mem for x A\<close> = (x, A)
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
 (*read a constructor specification*)
 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
     let val prems = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>o\<close>) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> \<^Type>\<open>i\<close>
                 handle TERM _ => error
                     "Bad variable in constructor specification"
     in ((id,T,syn), id, args, prems) end;
 
 val read_constructs = map o map o read_construct;
 
 (*convert constructor specifications into introduction rules*)
 fun mk_intr_tms sg (rec_tm, constructs) =
   let
     fun mk_intr ((id,T,syn), name, args, prems) =
       Logic.list_implies
         (map FOLogic.mk_Trueprop prems,
          FOLogic.mk_Trueprop
             (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
 
 fun mk_Un (t1, t2) = \<^Const>\<open>Un for t1 t2\<close>;
 
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = \<^Type>\<open>i\<close>)
   in  case filter is_ind (args @ cs) of
          [] => \<^Const>\<open>zero\<close>
        | u_args => Balanced_Tree.make mk_Un u_args
   end;
 
 
 (*Includes rules for succ and Pair since they are common constructions*)
 val elim_rls =
   [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
    @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
    make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
 
 
 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   | tryres (th, []) = raise THM("tryres", 0, [th]);
 
 fun gen_make_elim elim_rls rl =
   Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
 
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
 
 end;