diff --git a/src/FOL/fologic.ML b/src/FOL/fologic.ML
--- a/src/FOL/fologic.ML
+++ b/src/FOL/fologic.ML
@@ -1,102 +1,58 @@
 (*  Title:      FOL/fologic.ML
     Author:     Lawrence C Paulson
 
 Abstract syntax operations for FOL.
 *)
 
 signature FOLOGIC =
 sig
-  val oT: typ
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
-  val not: term
-  val conj: term
-  val disj: term
-  val imp: term
-  val iff: 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
-  val mk_binop: string -> term * term -> term
-  val mk_binrel: string -> term * term -> term
-  val dest_bin: string -> typ -> term -> term * term
 end;
 
 
 structure FOLogic: FOLOGIC =
 struct
 
-val oT = \<^Type>\<open>o\<close>;
-
-val Trueprop = \<^Const>\<open>Trueprop\<close>;
-
-fun mk_Trueprop P = Trueprop $ P;
-
-fun dest_Trueprop \<^Const_>\<open>Trueprop for P\<close> = P
-  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
-
-
-(* Logical constants *)
+fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
 
-val not = \<^Const>\<open>Not\<close>;
-val conj = \<^Const>\<open>conj\<close>;
-val disj = \<^Const>\<open>disj\<close>;
-val imp = \<^Const>\<open>imp\<close>;
-val iff = \<^Const>\<open>iff\<close>;
+val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
 
-fun mk_conj (t1, t2) = conj $ t1 $ t2
-and mk_disj (t1, t2) = disj $ t1 $ t2
-and mk_imp (t1, t2) = imp $ t1 $ t2
-and mk_iff (t1, t2) = iff $ t1 $ t2;
+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>;
 
-fun dest_imp \<^Const_>\<open>imp for A B\<close> = (A, B)
-  | dest_imp  t = raise TERM ("dest_imp", [t]);
+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];
 
-fun dest_iff \<^Const_>\<open>iff for A B\<close> = (A, B)
-  | dest_iff  t = raise TERM ("dest_iff", [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 dest_eq \<^Const_>\<open>eq _ for lhs rhs\<close> = (lhs, rhs)
-  | dest_eq t = raise TERM ("dest_eq", [t])
+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;
 
-
-(* binary operations and relations *)
-
-fun mk_binop c (t, u) =
-  let val T = fastype_of t in
-    Const (c, [T, T] ---> T) $ t $ u
-  end;
-
-fun mk_binrel c (t, u) =
-  let val T = fastype_of t in
-    Const (c, [T, T] ---> oT) $ t $ u
-  end;
-
-fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
-      if c = c' andalso T = T' then (t, u)
-      else raise TERM ("dest_bin " ^ c, [tm])
-  | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
-
 end;
diff --git a/src/FOL/simpdata.ML b/src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML
+++ b/src/FOL/simpdata.ML
@@ -1,152 +1,152 @@
 (*  Title:      FOL/simpdata.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Simplification data for FOL.
 *)
 
 (*Make meta-equalities.  The operator below is Trueprop*)
 
 fun mk_meta_eq th =
   (case Thm.concl_of th of
     _ $ \<^Const_>\<open>eq _ for _ _\<close> => th RS @{thm eq_reflection}
   | _ $ \<^Const_>\<open>iff for _ _\<close> => th RS @{thm iff_reflection}
   | _ => error "conclusion must be a =-equality or <->");
 
 fun mk_eq th =
   (case Thm.concl_of th of
     \<^Const_>\<open>Pure.eq _ for _ _\<close> => th
   | _ $ \<^Const_>\<open>eq _ for _ _\<close> => mk_meta_eq th
   | _ $ \<^Const_>\<open>iff for _ _\<close> => mk_meta_eq th
   | _ $ \<^Const_>\<open>Not for _\<close> => th RS @{thm iff_reflection_F}
   | _  => th RS @{thm iff_reflection_T});
 
 (*Replace premises x=y, X<->Y by X==Y*)
 fun mk_meta_prems ctxt =
     rule_by_tactic ctxt
       (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong ctxt rl =
   Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems ctxt rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");
 
 val mksimps_pairs =
   [(\<^const_name>\<open>imp\<close>, [@{thm mp}]), (\<^const_name>\<open>conj\<close>, [@{thm conjunct1}, @{thm conjunct2}]),
    (\<^const_name>\<open>All\<close>, [@{thm spec}]), (\<^const_name>\<open>True\<close>, []), (\<^const_name>\<open>False\<close>, [])];
 
 fun mk_atomize pairs =
   let
     fun atoms th =
       (case Thm.concl_of th of
          \<^Const_>\<open>Trueprop for p\<close> =>
            (case head_of p of
               Const(a,_) =>
                 (case AList.lookup (op =) pairs a of
                    SOME(rls) => maps atoms ([th] RL rls)
                  | NONE => [th])
             | _ => [th])
        | _ => [th])
   in atoms end;
 
 fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt;
 
 
 (** make simplification procedures for quantifier elimination **)
 structure Quantifier1 = Quantifier1
 (
   (*abstract syntax*)
   fun dest_eq \<^Const_>\<open>eq _ for s t\<close> = SOME (s, t)
     | dest_eq _ = NONE
   fun dest_conj \<^Const_>\<open>conj for s t\<close> = SOME (s, t)
     | dest_conj _ = NONE
   fun dest_imp \<^Const_>\<open>imp for s t\<close> = SOME (s, t)
     | dest_imp _ = NONE
-  val conj = FOLogic.conj
-  val imp  = FOLogic.imp
+  val conj = \<^Const>\<open>conj\<close>
+  val imp  = \<^Const>\<open>imp\<close>
   (*rules*)
   val iff_reflection = @{thm iff_reflection}
   val iffI = @{thm iffI}
   val iff_trans = @{thm iff_trans}
   val conjI= @{thm conjI}
   val conjE= @{thm conjE}
   val impI = @{thm impI}
   val mp   = @{thm mp}
   val uncurry = @{thm uncurry}
   val exI  = @{thm exI}
   val exE  = @{thm exE}
   val iff_allI = @{thm iff_allI}
   val iff_exI = @{thm iff_exI}
   val all_comm = @{thm all_comm}
   val ex_comm = @{thm ex_comm}
   val atomize =
     let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_iff atomize_conj}
     in fn ctxt => Raw_Simplifier.rewrite ctxt true rules end
 );
 
 
 (*** Case splitting ***)
 
 structure Splitter = Splitter
 (
   val context = \<^context>
   val mk_eq = mk_eq
   val meta_eq_to_iff = @{thm meta_eq_to_iff}
   val iffD = @{thm iffD2}
   val disjE = @{thm disjE}
   val conjE = @{thm conjE}
   val exE = @{thm exE}
   val contrapos = @{thm contrapos}
   val contrapos2 = @{thm contrapos2}
   val notnotD = @{thm notnotD}
   val safe_tac = Cla.safe_tac
 );
 
 val split_tac = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
 val split_asm_tac = Splitter.split_asm_tac;
 
 
 (*** Standard simpsets ***)
 
 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}];
 
 fun unsafe_solver ctxt =
   FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
     assume_tac ctxt,
     eresolve_tac ctxt @{thms FalseE}];
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =
   FIRST' [match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
     eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
   empty_simpset \<^context>
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)
   |> Simplifier.set_subgoaler asm_simp_tac
   |> Simplifier.set_mksimps (mksimps mksimps_pairs)
   |> Simplifier.set_mkcong mk_meta_cong
   |> simpset_of;
 
 fun unfold_tac ctxt ths =
   ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths));
 
 
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = Clasimp
 (
   structure Simplifier = Simplifier
     and Splitter = Splitter
     and Classical = Cla
     and Blast = Blast
   val iffD1 = @{thm iffD1}
   val iffD2 = @{thm iffD2}
   val notE = @{thm notE}
 );
 open Clasimp;
 
diff --git a/src/ZF/Tools/cartprod.ML b/src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML
+++ b/src/ZF/Tools/cartprod.ML
@@ -1,117 +1,115 @@
 (*  Title:      ZF/Tools/cartprod.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
 Signatures for inductive definitions.
 
 Syntactic operations for Cartesian Products.
 *)
 
 signature FP =          (** Description of a fixed point operator **)
   sig
   val oper      : term                  (*fixed point operator*)
   val bnd_mono  : term                  (*monotonicity predicate*)
   val bnd_monoI : thm                   (*intro rule for bnd_mono*)
   val subs      : thm                   (*subset theorem for fp*)
   val Tarski    : thm                   (*Tarski's fixed point theorem*)
   val induct    : thm                   (*induction/coinduction rule*)
   end;
 
 signature SU =                  (** Description of a disjoint sum **)
   sig
   val sum       : term                  (*disjoint sum operator*)
   val inl       : term                  (*left injection*)
   val inr       : term                  (*right injection*)
   val elim      : term                  (*case operator*)
   val case_inl  : thm                   (*inl equality rule for case*)
   val case_inr  : thm                   (*inr equality rule for case*)
   val inl_iff   : thm                   (*injectivity of inl, using <->*)
   val inr_iff   : thm                   (*injectivity of inr, using <->*)
   val distinct  : thm                   (*distinctness of inl, inr using <->*)
   val distinct' : thm                   (*distinctness of inr, inl using <->*)
   val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
   end;
 
 signature PR =                  (** Description of a Cartesian product **)
   sig
   val sigma     : term                  (*Cartesian product operator*)
   val pair      : term                  (*pairing operator*)
   val split_name : string               (*name of polymorphic split*)
   val pair_iff  : thm                   (*injectivity of pairing, using <->*)
   val split_eq  : thm                   (*equality rule for split*)
   val fsplitI   : thm                   (*intro rule for fsplit*)
   val fsplitD   : thm                   (*destruct rule for fsplit*)
   val fsplitE   : thm                   (*elim rule; apparently never used*)
   end;
 
 signature CARTPROD =            (** Derived syntactic functions for produts **)
   sig
   val ap_split : typ -> typ -> term -> term
   val factors : typ -> typ list
   val mk_prod : typ * typ -> typ
   val mk_tuple : term -> typ -> term list -> term
   val pseudo_type : term -> typ
   val remove_split : Proof.context -> thm -> thm
   val split_const : typ -> term
   val split_rule_var : Proof.context -> term * typ * thm -> thm
   end;
 
 
 functor CartProd_Fun (Pr: PR) : CARTPROD =
 struct
 
 (* Some of these functions expect "pseudo-types" containing products,
    as in HOL; the true ZF types would just be "i" *)
 
 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
 
 (*Bogus product type underlying a (possibly nested) Sigma.  
   Lets us share HOL code*)
 fun pseudo_type (t $ A $ Abs(_,_,B)) = 
       if t = Pr.sigma
       then mk_prod(pseudo_type A, pseudo_type B)
-      else \<^typ>\<open>i\<close>
-  | pseudo_type _ = \<^typ>\<open>i\<close>;
+      else \<^Type>\<open>i\<close>
+  | pseudo_type _ = \<^Type>\<open>i\<close>;
 
 (*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
 fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
   | factors T                     = [T];
 
 (*Make a well-typed instance of "split"*)
-fun split_const T = Const(Pr.split_name, 
-                          [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
-                           Ind_Syntax.iT] ---> T);
+fun split_const T = Const(Pr.split_name, [[\<^Type>\<open>i\<close>, \<^Type>\<open>i\<close>]--->T, \<^Type>\<open>i\<close>] ---> T);
 
 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument
   of type S.*)
 fun ap_split (Type("*", [T1,T2])) T3 u   = 
        split_const T3 $ 
-       Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
+       Abs("v", \<^Type>\<open>i\<close>, (*Not T1, as it involves pseudo-product types*)
            ap_split T2 T3
            ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
             Bound 0))
   | ap_split T T3 u = u;
 
 (*Makes a nested tuple from a list, following the product type structure*)
 fun mk_tuple pair (Type("*", [T1,T2])) tms = 
         pair $ mk_tuple pair T1 tms
              $ mk_tuple pair T2 (drop (length (factors T1)) tms)
   | mk_tuple pair T (t::_) = t;
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
 fun remove_split ctxt = rewrite_rule ctxt [Pr.split_eq];
 
 (*Uncurries any Var according to its "pseudo-product type" T1 in the rule*)
 fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
       let val T' = factors T1 ---> T2
           val newt = ap_split T1 T2 (Var(v,T'))
       in
         remove_split ctxt
           (Drule.instantiate_normalize (TVars.empty,
-            Vars.make [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
+            Vars.make [((v, \<^Type>\<open>i\<close> --> T2), Thm.cterm_of ctxt newt)]) rl)
       end
   | split_rule_var _ (t,T,rl) = rl;
 
 end;
 
diff --git a/src/ZF/Tools/datatype_package.ML b/src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML
+++ b/src/ZF/Tools/datatype_package.ML
@@ -1,452 +1,452 @@
 (*  Title:      ZF/Tools/datatype_package.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Datatype/Codatatype Definitions.
 
 The functor will be instantiated for normal sums/products (datatype defs)
                          and non-standard sums/products (codatatype defs)
 
 Sums are used only for mutual recursion;
 Products are used only to derive "streamlined" induction rules for relations
 *)
 
 type datatype_result =
    {con_defs   : thm list,             (*definitions made in thy*)
     case_eqns  : thm list,             (*equations for case operator*)
     recursor_eqns : thm list,          (*equations for the recursor*)
     free_iffs  : thm list,             (*freeness rewrite rules*)
     free_SEs   : thm list,             (*freeness destruct rules*)
     mk_free    : Proof.context -> string -> thm};    (*function to make freeness theorems*)
 
 signature DATATYPE_ARG =
 sig
   val intrs : thm list
   val elims : thm list
 end;
 
 signature DATATYPE_PACKAGE =
 sig
   (*Insert definitions for the recursive sets, which
      must *already* be declared as constants in parent theory!*)
   val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
     thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
   val add_datatype: string * string list -> (string * string list * mixfix) list list ->
     (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
     (Facts.ref * Token.src list) list -> theory -> theory * inductive_result * datatype_result
 end;
 
 functor Add_datatype_def_Fun
  (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
   and Ind_Package : INDUCTIVE_PACKAGE
   and Datatype_Arg : DATATYPE_ARG
   val coind : bool): DATATYPE_PACKAGE =
 struct
 
 (*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
 
 (*univ or quniv constitutes the sum domain for mutual recursion;
   it is applied to the datatype parameters and to Consts occurring in the
   definition other than Nat.nat and the datatype sets themselves.
   FIXME: could insert all constant set expressions, e.g. nat->nat.*)
 fun data_domain co (rec_tms, con_ty_lists) =
     let val rec_hds = map head_of rec_tms
         val dummy = rec_hds |> forall (fn t => is_Const t orelse
           error ("Datatype set not previously declared as constant: " ^
                    Syntax.string_of_term_global \<^theory>\<open>IFOL\<close> t));
         val rec_names = (*nat doesn't have to be added*)
             \<^const_name>\<open>nat\<close> :: map (#1 o dest_Const) rec_hds
         val u = if co then \<^Const>\<open>QUniv.quniv\<close> else \<^Const>\<open>Univ.univ\<close>
         val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
           (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
             | _ => I)) con_ty_lists [];
     in  u $ Ind_Syntax.union_params (hd rec_tms, cs)  end;
 
 fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
  let
   val rec_hds = map head_of rec_tms;
 
   val dummy = rec_hds |> forall (fn t => is_Const t orelse
           error ("Datatype set not previously declared as constant: " ^
                    Syntax.string_of_term_global thy t));
 
   val rec_names = map (#1 o dest_Const) rec_hds
   val rec_base_names = map Long_Name.base_name rec_names
   val big_rec_base_name = space_implode "_" rec_base_names
 
   val thy_path = thy |> Sign.add_path big_rec_base_name
 
   val big_rec_name = Sign.intern_const thy_path big_rec_base_name;
 
   val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists);
 
   val dummy =
     writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
 
   val case_varname = "f";                (*name for case variables*)
 
   (** Define the constructors **)
 
   (*The empty tuple is 0*)
   fun mk_tuple [] = \<^Const>\<open>zero\<close>
     | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
 
   fun mk_inject n k u = Balanced_Tree.access
     {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k;
 
   val npart = length rec_names;  (*number of mutually recursive parts*)
 
 
   val full_name = Sign.full_bname thy_path;
 
   (*Make constructor definition;
     kpart is the number of this mutually recursive part*)
   fun mk_con_defs (kpart, con_ty_list) =
     let val ncon = length con_ty_list    (*number of constructors*)
         fun mk_def (((id,T,syn), name, args, prems), kcon) =
               (*kcon is index of constructor*)
             Misc_Legacy.mk_defpair (list_comb (Const (full_name name, T), args),
                         mk_inject npart kpart
                         (mk_inject ncon kcon (mk_tuple args)))
     in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
 
 
   (*** Define the case operator ***)
 
   (*Combine split terms using case; yields the case operator for one part*)
   fun call_case case_list =
-    let fun call_f (free,[]) = Abs("null", \<^typ>\<open>i\<close>, free)
+    let fun call_f (free,[]) = Abs("null", \<^Type>\<open>i\<close>, free)
           | call_f (free,args) =
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
-                            \<^typ>\<open>i\<close>
+                            \<^Type>\<open>i\<close>
                             free
     in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
 
   (** Generating function variables for the case definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
 
   (*The function variable for a single constructor*)
   fun add_case ((_, T, _), name, args, _) (opno, cases) =
     if Symbol_Pos.is_identifier name then
       (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
     else
       (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
        :: cases);
 
   (*Treatment of a list of constructors, for one part
     Result adds a list of terms, each a function variable with arguments*)
   fun add_case_list con_ty_list (opno, case_lists) =
     let val (opno', case_list) = fold_rev add_case con_ty_list (opno, [])
     in (opno', case_list :: case_lists) end;
 
   (*Treatment of all parts*)
   val (_, case_lists) = fold_rev add_case_list con_ty_lists (1, []);
 
   (*extract the types of all the variables*)
   val case_typ = maps (map (#2 o #1)) con_ty_lists ---> \<^typ>\<open>i => i\<close>;
 
   val case_base_name = big_rec_base_name ^ "_case";
   val case_name = full_name case_base_name;
 
   (*The list of all the function variables*)
   val case_args = maps (map #1) case_lists;
 
   val case_const = Const (case_name, case_typ);
   val case_tm = list_comb (case_const, case_args);
 
   val case_def = Misc_Legacy.mk_defpair
     (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
 
 
   (** Generating function variables for the recursor definition
       Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
 
   (*a recursive call for x is the application rec`x  *)
-  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
+  val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^Type>\<open>i\<close>);
 
   (*look back down the "case args" (which have been reversed) to
     determine the de Bruijn index*)
   fun make_rec_call ([], _) arg = error
           "Internal error in datatype (variable name mismatch)"
     | make_rec_call (a::args, i) arg =
            if a = arg then rec_call $ Bound i
            else make_rec_call (args, i+1) arg;
 
   (*creates one case of the "X_case" definition of the recursor*)
   fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =
       let fun add_abs (Free(a,T), u) = Abs(a,T,u)
           val ncase_args = length case_args
           val bound_args = map Bound ((ncase_args - 1) downto 0)
           val rec_args = map (make_rec_call (rev case_args,0))
                          (List.drop(recursor_args, ncase_args))
       in
           List.foldr add_abs
             (list_comb (recursor_var,
                         bound_args @ rec_args)) case_args
       end
 
   (*Find each recursive argument and add a recursive call for it*)
   fun rec_args [] = []
     | rec_args (\<^Const_>\<open>mem for arg X\<close>::prems) =
        (case head_of X of
             Const(a,_) => (*recursive occurrence?*)
                           if member (op =) rec_names a
                               then arg :: rec_args prems
                           else rec_args prems
           | _ => rec_args prems)
     | rec_args (_::prems) = rec_args prems;
 
   (*Add an argument position for each occurrence of a recursive set.
     Strictly speaking, the recursive arguments are the LAST of the function
     variable, but they all have type "i" anyway*)
-  fun add_rec_args args' T = (map (fn _ => \<^typ>\<open>i\<close>) args') ---> T
+  fun add_rec_args args' T = (map (fn _ => \<^Type>\<open>i\<close>) args') ---> T
 
   (*Plug in the function variable type needed for the recursor
     as well as the new arguments (recursive calls)*)
   fun rec_ty_elem ((id, T, syn), name, args, prems) =
       let val args' = rec_args prems
       in ((id, add_rec_args args' T, syn),
           name, args @ args', prems)
       end;
 
   val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
 
   (*Treatment of all parts*)
   val (_, recursor_lists) = fold_rev add_case_list rec_ty_lists (1, []);
 
   (*extract the types of all the variables*)
   val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> \<^typ>\<open>i => i\<close>;
 
   val recursor_base_name = big_rec_base_name ^ "_rec";
   val recursor_name = full_name recursor_base_name;
 
   (*The list of all the function variables*)
   val recursor_args = maps (map #1) recursor_lists;
 
   val recursor_tm =
     list_comb (Const (recursor_name, recursor_typ), recursor_args);
 
   val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
 
   val recursor_def =
       Misc_Legacy.mk_defpair
         (recursor_tm,
          \<^Const>\<open>Univ.Vrecursor\<close> $
-           absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
+           absfree ("rec", \<^Type>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)
 
   val need_recursor = (not coind andalso recursor_typ <> case_typ);
 
   fun add_recursor thy =
     if need_recursor then
       thy
       |> Sign.add_consts [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
       |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
     else thy;
 
   val (con_defs, thy0) = thy_path
     |> Sign.add_consts
         (map (fn (c, T, mx) => (Binding.name c, T, mx))
          ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
     |> Global_Theory.add_defs false
         (map (Thm.no_attributes o apfst Binding.name)
          (case_def ::
           flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
     ||> add_recursor
     ||> Sign.parent_path;
 
   val intr_names = map (Binding.name o #2) (flat con_ty_lists);
   val (thy1, ind_result) =
     thy0 |> Ind_Package.add_inductive_i
       false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
       (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims);
 
   (**** Now prove the datatype theorems in this theory ****)
 
 
   (*** Prove the case theorems ***)
 
   (*Each equation has the form
     case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
   fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
     FOLogic.mk_Trueprop
       (FOLogic.mk_eq
        (case_tm $
          (list_comb (Const (Sign.intern_const thy1 name,T),
                      args)),
         list_comb (case_free, args)));
 
   val case_trans = hd con_defs RS @{thm def_trans}
   and split_trans = Pr.split_eq RS @{thm meta_eq_to_obj_eq} RS @{thm trans};
 
   fun prove_case_eqn (arg, con_def) =
     Goal.prove_global thy1 [] []
       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
       (fn {context = ctxt, ...} => EVERY
         [rewrite_goals_tac ctxt [con_def],
          resolve_tac ctxt [case_trans] 1,
          REPEAT
            (resolve_tac ctxt [@{thm refl}, split_trans,
              Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
 
   val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]);
 
   val ([case_eqns], thy2) = thy1
     |> Sign.add_path big_rec_base_name
     |> Global_Theory.add_thmss
       [((Binding.name "case_eqns",
           map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs)), [])]
     ||> Sign.parent_path;
 
 
   (*** Prove the recursor theorems ***)
 
   val (recursor_eqns, thy3) =
    case try (Misc_Legacy.get_def thy2) recursor_base_name of
      NONE => (writeln "  [ No recursion operator ]";
               ([], thy2))
    | SOME recursor_def =>
       let
         (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
         fun subst_rec \<^Const_>\<open>apply for \<open>Free _\<close> arg\<close> = recursor_tm $ arg
           | subst_rec tm =
               let val (head, args) = strip_comb tm
               in  list_comb (head, map subst_rec args)  end;
 
         (*Each equation has the form
           REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
           where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
           constructor argument.*)
         fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
           FOLogic.mk_Trueprop
            (FOLogic.mk_eq
             (recursor_tm $
              (list_comb (Const (Sign.intern_const thy2 name,T),
                          args)),
              subst_rec (Term.betapplys (recursor_case, args))));
 
         val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS @{thm trans};
 
         fun prove_recursor_eqn arg =
           Goal.prove_global thy2 [] []
             (Ind_Syntax.traceIt "next recursor equation = " thy2 (mk_recursor_eqn arg))
             (*Proves a single recursor equation.*)
             (fn {context = ctxt, ...} => EVERY
               [resolve_tac ctxt [recursor_trans] 1,
                simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1,
                IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]);
       in
         thy2
         |> Sign.add_path big_rec_base_name
         |> Global_Theory.add_thmss
           [((Binding.name "recursor_eqns",
             map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)), [])]
         ||> Sign.parent_path
         |>> the_single
       end
 
   val constructors =
       map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
 
   val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
 
   val {intrs, elim, induct, mutual_induct, ...} = ind_result
 
   (*Typical theorems have the form ~con1=con2, con1=con2==>False,
     con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   fun mk_free ctxt s =
     let
       val thy = Proof_Context.theory_of ctxt;
     in
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
         (fn {context = ctxt', ...} => EVERY
          [rewrite_goals_tac ctxt' con_defs,
           fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])
     end;
 
   val dt_info =
         {inductive = true,
          constructors = constructors,
          rec_rewrites = map Thm.trim_context recursor_eqns,
          case_rewrites = map Thm.trim_context case_eqns,
          induct = Thm.trim_context induct,
          mutual_induct = Thm.trim_context mutual_induct,
          exhaustion = Thm.trim_context elim};
 
   val con_info =
         {big_rec_name = big_rec_name,
          constructors = constructors,
             (*let primrec handle definition by cases*)
          free_iffs = map Thm.trim_context free_iffs,
          rec_rewrites =
           (case recursor_eqns of [] => case_eqns | _ => recursor_eqns)
           |> map Thm.trim_context};
 
   (*associate with each constructor the datatype name and rewrites*)
   val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
 
  in
   (*Updating theory components: simprules and datatype info*)
   (thy3 |> Sign.add_path big_rec_base_name
         |> Global_Theory.add_thmss
          [((Binding.name "simps", case_eqns @ recursor_eqns), [Simplifier.simp_add]),
           ((Binding.empty, intrs), [Cla.safe_intro NONE]),
           ((Binding.name "con_defs", con_defs), []),
           ((Binding.name "free_iffs", free_iffs), []),
           ((Binding.name "free_elims", free_SEs), [])] |> #2
         |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
         |> ConstructorsData.map (fold Symtab.update con_pairs)
         |> Sign.parent_path,
    ind_result,
    {con_defs = con_defs,
     case_eqns = case_eqns,
     recursor_eqns = recursor_eqns,
     free_iffs = free_iffs,
     free_SEs = free_SEs,
     mk_free = mk_free})
   end;
 
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = Proof_Context.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> Type.constraint \<^typ>\<open>i\<close>) strs
+      map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;
     val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists;
     val dom_sum =
       if sdom = "" then data_domain coind (rec_tms, con_ty_lists)
       else singleton read_is sdom;
     val monos = Attrib.eval_thms ctxt raw_monos;
     val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
     val type_elims = Attrib.eval_thms ctxt raw_type_elims;
   in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
 
 
 (* outer syntax *)
 
 fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
   #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
 
 val con_decl =
   Parse.name -- Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.list1 Parse.term --| \<^keyword>\<open>)\<close>) [] --
     Parse.opt_mixfix >> Scan.triple1;
 
 val coind_prefix = if coind then "co" else "";
 
 val _ =
   Outer_Syntax.command
     (if coind then \<^command_keyword>\<open>codatatype\<close> else \<^command_keyword>\<open>datatype\<close>)
     ("define " ^ coind_prefix ^ "datatype")
     ((Scan.optional ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><=\<close>) |-- Parse.!!! Parse.term) "") --
       Parse.and_list1 (Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.enum1 "|" con_decl)) --
       Scan.optional (\<^keyword>\<open>monos\<close> |-- Parse.!!! Parse.thms1) [] --
       Scan.optional (\<^keyword>\<open>type_intros\<close> |-- Parse.!!! Parse.thms1) [] --
       Scan.optional (\<^keyword>\<open>type_elims\<close> |-- Parse.!!! Parse.thms1) []
       >> (Toplevel.theory o mk_datatype));
 
 end;
 
diff --git a/src/ZF/Tools/inductive_package.ML b/src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML
+++ b/src/ZF/Tools/inductive_package.ML
@@ -1,609 +1,609 @@
 (*  Title:      ZF/Tools/inductive_package.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Fixedpoint definition module -- for Inductive/Coinductive Definitions
 
 The functor will be instantiated for normal sums/products (inductive defs)
                          and non-standard sums/products (coinductive defs)
 
 Sums are used only for mutual recursion;
 Products are used only to derive "streamlined" induction rules for relations
 *)
 
 type inductive_result =
    {defs       : thm list,             (*definitions made in thy*)
     bnd_mono   : thm,                  (*monotonicity for the lfp definition*)
     dom_subset : thm,                  (*inclusion of recursive set in dom*)
     intrs      : thm list,             (*introduction rules*)
     elim       : thm,                  (*case analysis theorem*)
     induct     : thm,                  (*main induction rule*)
     mutual_induct : thm};              (*mutual induction rule*)
 
 
 (*Functor's result signature*)
 signature INDUCTIVE_PACKAGE =
 sig
   (*Insert definitions for the recursive sets, which
      must *already* be declared as constants in parent theory!*)
   val add_inductive_i: bool -> term list * term ->
     ((binding * term) * attribute list) list ->
     thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   val add_inductive: string list * string ->
     ((binding * string) * Token.src list) list ->
     (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
     (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list ->
     theory -> theory * inductive_result
 end;
 
 
 (*Declares functions to add fixedpoint/constructor defs to a theory.
   Recursive sets must *already* be declared as constants.*)
 functor Add_inductive_def_Fun
     (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool)
  : INDUCTIVE_PACKAGE =
 struct
 
 val co_prefix = if coind then "co" else "";
 
 
 (* utils *)
 
 (*make distinct individual variables a1, a2, a3, ..., an. *)
 fun mk_frees a [] = []
   | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts;
 
 
 (* add_inductive(_i) *)
 
 (*internal version, accepting terms*)
 fun add_inductive_i verbose (rec_tms, dom_sum)
   raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy0 =
 let
   val ctxt0 = Proof_Context.init_global thy0;
 
   val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
   val (intr_names, intr_tms) = split_list (map fst intr_specs);
   val case_names = Rule_Cases.case_names intr_names;
 
   (*recT and rec_params should agree for all mutually recursive components*)
   val rec_hds = map head_of rec_tms;
 
   val dummy = rec_hds |> forall (fn t => is_Const t orelse
       error ("Recursive set not previously declared as constant: " ^
                    Syntax.string_of_term ctxt0 t));
 
   (*Now we know they are all Consts, so get their names, type and params*)
   val rec_names = map (#1 o dest_Const) rec_hds
   and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
 
   val rec_base_names = map Long_Name.base_name rec_names;
   val dummy = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse
     error ("Base name of recursive set not an identifier: " ^ a));
 
   local (*Checking the introduction rules*)
     val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy0) intr_tms;
     fun intr_ok set =
         case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
   in
     val dummy = intr_sets |> forall (fn t => intr_ok t orelse
       error ("Conclusion of rule does not name a recursive set: " ^
                 Syntax.string_of_term ctxt0 t));
   end;
 
   val dummy = rec_params |> forall (fn t => is_Free t orelse
       error ("Param in recursion term not a free variable: " ^
                Syntax.string_of_term ctxt0 t));
 
   (*** Construct the fixedpoint definition ***)
   val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
   fun dest_tprop \<^Const_>\<open>Trueprop for P\<close> = P
     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
                             Syntax.string_of_term ctxt0 Q);
 
   (*Makes a disjunct from an introduction rule*)
   fun fp_part intr = (*quantify over rule's free vars except parameters*)
     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
         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', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl 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
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
-  fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*)
-    | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
+  fun mk_Part (Bound 0) = Free(X', \<^Type>\<open>i\<close>) (*no mutual rec, no Part needed*)
+    | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', \<^Type>\<open>i\<close>) $ Abs (w', \<^Type>\<open>i\<close>, h);
 
   (*Access to balanced disjoint sums via injections*)
   val parts = map mk_Part
     (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
       (length rec_tms));
 
   (*replace each set by the corresponding Part(A,h)*)
   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
 
   val fp_abs =
-    absfree (X', Ind_Syntax.iT)
+    absfree (X', \<^Type>\<open>i\<close>)
         (Ind_Syntax.mk_Collect (z', dom_sum,
             Balanced_Tree.make FOLogic.mk_disj part_intrs));
 
   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
 
   val dummy = List.app (fn rec_hd => (Logic.occs (rec_hd, fp_rhs) andalso
                              error "Illegal occurrence of recursion operator"; ()))
            rec_hds;
 
   (*** Make the new theory ***)
 
   (*A key definition:
     If no mutual recursion then it equals the one recursive set.
     If mutual recursion then it differs from all the recursive sets. *)
   val big_rec_base_name = space_implode "_" rec_base_names;
   val big_rec_name = Proof_Context.intern_const ctxt0 big_rec_base_name;
 
 
   val _ =
     if verbose then
       writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)
     else ();
 
   (*Big_rec... is the union of the mutually recursive sets*)
   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
   (*The individual sets must already be declared*)
   val axpairs = map Misc_Legacy.mk_defpair
         ((big_rec_tm, fp_rhs) ::
          (case parts of
              [_] => []                        (*no mutual recursion*)
            | _ => rec_tms ~~          (*define the sets as Parts*)
-                  map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts));
+                  map (subst_atomic [(Free (X', \<^Type>\<open>i\<close>), big_rec_tm)]) parts));
 
   (*tracing: print the fixedpoint definition*)
   val dummy = if !Ind_Syntax.trace then
               writeln (cat_lines (map (Syntax.string_of_term ctxt0 o #2) axpairs))
           else ()
 
   (*add definitions of the inductive sets*)
   val (_, thy1) =
     thy0
     |> Sign.add_path big_rec_base_name
     |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
 
 
   (*fetch fp definitions from the theory*)
   val big_rec_def::part_rec_defs =
     map (Misc_Legacy.get_def thy1)
         (case rec_names of [_] => rec_names
                          | _   => big_rec_base_name::rec_names);
 
 
   (********)
   val dummy = writeln "  Proving monotonicity...";
 
   val bnd_mono0 =
     Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
       (fn {context = ctxt, ...} => EVERY
         [resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
          REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
 
   val dom_subset0 = Drule.export_without_context (big_rec_def RS Fp.subs);
 
   val ([bnd_mono, dom_subset], thy2) = thy1
     |> Global_Theory.add_thms
       [((Binding.name "bnd_mono", bnd_mono0), []),
        ((Binding.name "dom_subset", dom_subset0), [])];
 
   val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski);
 
 
   (********)
   val dummy = writeln "  Proving the introduction rules...";
 
   (*Mutual recursion?  Helps to derive subset rules for the
     individual sets.*)
   val Part_trans =
       case rec_names of
            [_] => asm_rl
          | _   => Drule.export_without_context (@{thm Part_subset} RS @{thm subset_trans});
 
   (*To type-check recursive occurrences of the inductive sets, possibly
     enclosed in some monotonic operator M.*)
   val rec_typechecks =
      [dom_subset] RL (asm_rl :: ([Part_trans] RL monos))
      RL [@{thm subsetD}];
 
   (*Type-checking is hardest aspect of proof;
     disjIn selects the correct disjunct after unfolding*)
   fun intro_tacsf disjIn ctxt =
     [DETERM (stac ctxt unfold 1),
      REPEAT (resolve_tac ctxt [@{thm Part_eqI}, @{thm CollectI}] 1),
      (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
      resolve_tac ctxt [disjIn] 2,
      (*Not ares_tac, since refl must be tried before equality assumptions;
        backtracking may occur if the premises have extra variables!*)
      DEPTH_SOLVE_1 (resolve_tac ctxt [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac ctxt 2),
      (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
      rewrite_goals_tac ctxt con_defs,
      REPEAT (resolve_tac ctxt @{thms refl} 2),
      (*Typechecking; this can fail*)
      if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
      else all_tac,
      REPEAT (FIRSTGOAL (dresolve_tac ctxt rec_typechecks
                         ORELSE' eresolve_tac ctxt (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
                                               type_elims)
                         ORELSE' hyp_subst_tac ctxt)),
      if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
      else all_tac,
      DEPTH_SOLVE (swap_res_tac ctxt (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
 
   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   val mk_disj_rls = Balanced_Tree.accesses
     {left = fn rl => rl RS @{thm disjI1},
      right = fn rl => rl RS @{thm disjI2},
      init = @{thm asm_rl}};
 
   val intrs0 =
     (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
     |> ListPair.map (fn (t, tacs) =>
       Goal.prove_global thy2 [] [] t
         (fn {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt)));
 
   val ([intrs], thy3) = thy2
     |> Global_Theory.add_thmss [((Binding.name "intros", intrs0), [])];
 
   val ctxt3 = Proof_Context.init_global thy3;
 
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";
 
   (*Breaks down logical connectives in the monotonic function*)
   fun basic_elim_tac ctxt =
       REPEAT (SOMEGOAL (eresolve_tac ctxt (Ind_Syntax.elim_rls @ Su.free_SEs)
                 ORELSE' bound_hyp_subst_tac ctxt))
       THEN prune_params_tac ctxt
           (*Mutual recursion: collapse references to Part(D,h)*)
       THEN (PRIMITIVE (fold_rule ctxt part_rec_defs));
 
   (*Elimination*)
   val (elim, thy4) = thy3
     |> Global_Theory.add_thm
       ((Binding.name "elim",
         rule_by_tactic ctxt3 (basic_elim_tac ctxt3) (unfold RS Ind_Syntax.equals_CollectD)), []);
 
   val ctxt4 = Proof_Context.init_global thy4;
 
   (*Applies freeness of the given constructors, which *must* be unfolded by
       the given defs.  Cannot simply use the local con_defs because
       con_defs=[] for inference systems.
     Proposition A should have the form t:Si where Si is an inductive set*)
   fun make_cases ctxt A =
     rule_by_tactic ctxt
       (basic_elim_tac ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt)
       (Thm.assume A RS elim)
       |> Drule.export_without_context_open;
 
   fun induction_rules raw_induct =
    let
      val dummy = writeln "  Proving the induction rule...";
 
      (*** Prove the main induction rule ***)
 
      val pred_name = "P";            (*name for predicate variables*)
 
      (*Used to make induction rules;
         ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
         prem is a premise of an intr rule*)
      fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
           (case AList.lookup (op aconv) ind_alist X of
                SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
                  let fun mk_sb (rec_tm,pred) =
                              (rec_tm, \<^Const>\<open>Collect\<close> $ rec_tm $ pred)
                  in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
        | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
 
      (*Make a premise of the induction rule.*)
      fun induct_prem ind_alist intr =
        let val xs = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
            val iprems = List.foldr (add_induct_prem ind_alist) []
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr
            val (SOME pred) = AList.lookup (op aconv) ind_alist X
            val concl = FOLogic.mk_Trueprop (pred $ t)
        in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end
        handle Bind => error"Recursion term not found in conclusion";
 
      (*Minimizes backtracking by delivering the correct premise to each goal.
        Intro rules with extra Vars in premises still cause some backtracking *)
      fun ind_tac _ [] 0 = all_tac
        | ind_tac ctxt (prem::prems) i =
              DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1);
 
-     val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
+     val pred = Free(pred_name, \<^Type>\<open>i\<close> --> \<^Type>\<open>o\<close>);
 
      val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
                          intr_tms;
 
      val dummy =
       if ! Ind_Syntax.trace then
         writeln (cat_lines
           (["ind_prems:"] @ map (Syntax.string_of_term ctxt4) ind_prems @
            ["raw_induct:", Thm.string_of_thm ctxt4 raw_induct]))
       else ();
 
 
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
      val min_ss =
            (empty_simpset ctxt4
              |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
            setSolver (mk_solver "minimal"
                       (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
                                    ORELSE' assume_tac ctxt
                                    ORELSE' eresolve_tac ctxt @{thms FalseE}));
 
      val quant_induct =
        Goal.prove_global thy4 [] ind_prems
          (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
          (fn {context = ctxt, prems} => EVERY
            [rewrite_goals_tac ctxt part_rec_defs,
             resolve_tac ctxt [@{thm impI} RS @{thm allI}] 1,
             DETERM (eresolve_tac ctxt [raw_induct] 1),
             (*Push Part inside Collect*)
             full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
             (*This CollectE and disjE separates out the introduction rules*)
             REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm disjE}])),
             (*Now break down the individual cases.  No disjE here in case
               some premise involves disjunction.*)
             REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm exE}, @{thm conjE}]
                                ORELSE' (bound_hyp_subst_tac ctxt))),
             ind_tac ctxt (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
 
      val dummy =
       if ! Ind_Syntax.trace then
         writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt4 quant_induct)
       else ();
 
 
      (*** Prove the simultaneous induction rule ***)
 
      (*Make distinct predicates for each inductive set*)
 
      (*The components of the element type, several if it is a product*)
      val elem_type = CP.pseudo_type dom_sum;
      val elem_factors = CP.factors elem_type;
      val elem_frees = mk_frees "za" elem_factors;
      val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
 
      (*Given a recursive set and its domain, return the "fsplit" predicate
        and a conclusion for the simultaneous induction rule.
        NOTE.  This will not work for mutually recursive predicates.  Previously
        a summand 'domt' was also an argument, but this required the domain of
        mutual recursion to invariably be a disjoint sum.*)
      fun mk_predpair rec_tm =
        let val rec_name = (#1 o dest_Const o head_of) rec_tm
            val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
-                            elem_factors ---> FOLogic.oT)
+                            elem_factors ---> \<^Type>\<open>o\<close>)
            val qconcl =
              List.foldr FOLogic.mk_all
-               (FOLogic.imp $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
+               (\<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
                       $ (list_comb (pfree, elem_frees))) elem_frees
-       in  (CP.ap_split elem_type FOLogic.oT pfree,
+       in  (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
             qconcl)
        end;
 
      val (preds,qconcls) = split_list (map mk_predpair rec_tms);
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
-         FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
+         \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
 
      (*To instantiate the main induction rule*)
      val induct_concl =
          FOLogic.mk_Trueprop
            (Ind_Syntax.mk_all_imp
             (big_rec_tm,
-             Abs("z", Ind_Syntax.iT,
+             Abs("z", \<^Type>\<open>i\<close>,
                  Balanced_Tree.make FOLogic.mk_conj
                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
      and mutual_induct_concl =
       FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln ("induct_concl = " ^
                            Syntax.string_of_term ctxt4 induct_concl);
                   writeln ("mutual_induct_concl = " ^
                            Syntax.string_of_term ctxt4 mutual_induct_concl))
              else ();
 
 
      fun lemma_tac ctxt =
       FIRST' [eresolve_tac ctxt [@{thm asm_rl}, @{thm conjE}, @{thm PartE}, @{thm mp}],
               resolve_tac ctxt [@{thm allI}, @{thm impI}, @{thm conjI}, @{thm Part_eqI}],
               dresolve_tac ctxt [@{thm spec}, @{thm mp}, Pr.fsplitD]];
 
      val need_mutual = length rec_names > 1;
 
      val lemma = (*makes the link between the two induction rules*)
        if need_mutual then
           (writeln "  Proving the mutual induction rule...";
            Goal.prove_global thy4 [] []
              (Logic.mk_implies (induct_concl, mutual_induct_concl))
              (fn {context = ctxt, ...} => EVERY
                [rewrite_goals_tac ctxt part_rec_defs,
                 REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac ctxt 1)]))
        else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
 
      val dummy =
       if ! Ind_Syntax.trace then
         writeln ("lemma: " ^ Thm.string_of_thm ctxt4 lemma)
       else ();
 
 
      (*Mutual induction follows by freeness of Inl/Inr.*)
 
      (*Simplification largely reduces the mutual induction rule to the
        standard rule*)
      val mut_ss =
          min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
 
      val all_defs = con_defs @ part_rec_defs;
 
      (*Removes Collects caused by M-operators in the intro rules.  It is very
        hard to simplify
          list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))})
        where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
        Instead the following rules extract the relevant conjunct.
      *)
      val cmonos = [@{thm subset_refl} RS @{thm Collect_mono}] RL monos
                    RLN (2,[@{thm rev_subsetD}]);
 
      (*Minimizes backtracking by delivering the correct premise to each goal*)
      fun mutual_ind_tac _ [] 0 = all_tac
        | mutual_ind_tac ctxt (prem::prems) i =
            DETERM
             (SELECT_GOAL
                (
                 (*Simplify the assumptions and goal by unfolding Part and
                   using freeness of the Sum constructors; proves all but one
                   conjunct by contradiction*)
                 rewrite_goals_tac ctxt all_defs  THEN
                 simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1  THEN
                 IF_UNSOLVED (*simp_tac may have finished it off!*)
                   ((*simplify assumptions*)
                    (*some risk of excessive simplification here -- might have
                      to identify the bare minimum set of rewrites*)
                    full_simp_tac
                       (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
                    THEN
                    (*unpackage and use "prem" in the corresponding place*)
                    REPEAT (resolve_tac ctxt @{thms impI} 1)  THEN
                    resolve_tac ctxt [rewrite_rule ctxt all_defs prem] 1  THEN
                    (*prem must not be REPEATed below: could loop!*)
                    DEPTH_SOLVE (FIRSTGOAL (ares_tac ctxt [@{thm impI}] ORELSE'
                                            eresolve_tac ctxt (@{thm conjE} :: @{thm mp} :: cmonos))))
                ) i)
             THEN mutual_ind_tac ctxt prems (i-1);
 
      val mutual_induct_fsplit =
        if need_mutual then
          Goal.prove_global thy4 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
            mutual_induct_concl
            (fn {context = ctxt, prems} => EVERY
              [resolve_tac ctxt [quant_induct RS lemma] 1,
               mutual_ind_tac ctxt (rev prems) (length prems)])
        else @{thm TrueI};
 
      (** Uncurrying the predicate in the ordinary induction rule **)
 
      (*instantiate the variable to a tuple, if it is non-trivial, in order to
        allow the predicate to be "opened up".
        The name "x.1" comes from the "RS spec" !*)
      val inst =
          case elem_frees of [_] => I
             | _ => Drule.instantiate_normalize (TVars.empty,
                     Vars.make [(\<^var>\<open>?x1::i\<close>, Thm.global_cterm_of thy4 elem_tuple)]);
 
      (*strip quantifier and the implication*)
      val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
 
      val \<^Const_>\<open>Trueprop for \<open>pred_var $ _\<close>\<close> = Thm.concl_of induct0
 
      val induct0 =
        CP.split_rule_var ctxt4
-        (pred_var, elem_type-->FOLogic.oT, induct0)
+        (pred_var, elem_type --> \<^Type>\<open>o\<close>, induct0)
        |> Drule.export_without_context
      and mutual_induct = CP.remove_split ctxt4 mutual_induct_fsplit
 
      val ([induct, mutual_induct], thy5) =
        thy4
        |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct0),
              [case_names, Induct.induct_pred big_rec_name]),
            ((Binding.name "mutual_induct", mutual_induct), [case_names])];
     in ((induct, mutual_induct), thy5)
     end;  (*of induction_rules*)
 
   val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
 
   val ((induct, mutual_induct), thy5) =
     if not coind then induction_rules raw_induct
     else
       thy4
       |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
       |> apfst (hd #> pair @{thm TrueI});
 
 
   val (([cases], [defs]), thy6) =
     thy5
     |> IndCases.declare big_rec_name make_cases
     |> Global_Theory.add_thms
       [((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
     ||>> (Global_Theory.add_thmss o map Thm.no_attributes)
       [(Binding.name "defs", big_rec_def :: part_rec_defs)];
   val (named_intrs, thy7) =
     thy6
     |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs) ~~ map #2 intr_specs)
     ||> Sign.parent_path;
   in
     (thy7,
       {defs = defs,
        bnd_mono = bnd_mono,
        dom_subset = dom_subset,
        intrs = named_intrs,
        elim = cases,
        induct = induct,
        mutual_induct = mutual_induct})
   end;
 
 (*source version*)
 fun add_inductive (srec_tms, sdom_sum) intr_srcs
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
+    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>)
       #> Syntax.check_terms ctxt;
 
     val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs;
     val sintrs = map fst intr_srcs ~~ intr_atts;
     val rec_tms = read_terms srec_tms;
     val dom_sum = singleton read_terms sdom_sum;
     val intr_tms = Syntax.read_props ctxt (map (snd o fst) sintrs);
     val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
     val monos = Attrib.eval_thms ctxt raw_monos;
     val con_defs = Attrib.eval_thms ctxt raw_con_defs;
     val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
     val type_elims = Attrib.eval_thms ctxt raw_type_elims;
   in
     thy
     |> add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims)
   end;
 
 
 (* outer syntax *)
 
 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   #1 o add_inductive doms (map (fn ((x, y), z) => ((x, z), y)) intrs)
     (monos, con_defs, type_intrs, type_elims);
 
 val ind_decl =
   (\<^keyword>\<open>domains\<close> |-- Parse.!!! (Parse.enum1 "+" Parse.term --
       ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><=\<close>) |-- Parse.term))) --
   (\<^keyword>\<open>intros\<close> |--
     Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
   Scan.optional (\<^keyword>\<open>monos\<close> |-- Parse.!!! Parse.thms1) [] --
   Scan.optional (\<^keyword>\<open>con_defs\<close> |-- Parse.!!! Parse.thms1) [] --
   Scan.optional (\<^keyword>\<open>type_intros\<close> |-- Parse.!!! Parse.thms1) [] --
   Scan.optional (\<^keyword>\<open>type_elims\<close> |-- Parse.!!! Parse.thms1) []
   >> (Toplevel.theory o mk_ind);
 
 val _ =
   Outer_Syntax.command
     (if coind then \<^command_keyword>\<open>coinductive\<close> else \<^command_keyword>\<open>inductive\<close>)
     ("define " ^ co_prefix ^ "inductive sets") ind_decl;
 
 end;
 
diff --git a/src/ZF/Tools/primrec_package.ML b/src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML
+++ b/src/ZF/Tools/primrec_package.ML
@@ -1,203 +1,203 @@
 (*  Title:      ZF/Tools/primrec_package.ML
     Author:     Norbert Voelker, FernUni Hagen
     Author:     Stefan Berghofer, TU Muenchen
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Package for defining functions on datatypes by primitive recursion.
 *)
 
 signature PRIMREC_PACKAGE =
 sig
   val primrec: ((binding * string) * Token.src list) list -> theory -> thm list * theory
   val primrec_i: ((binding * term) * attribute list) list -> theory -> thm list * theory
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
 struct
 
 exception RecError of string;
 
 (*Remove outer Trueprop and equality sign*)
 val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
 
 fun primrec_err s = error ("Primrec definition error:\n" ^ s);
 
 fun primrec_eq_err sign s eq =
   primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq);
 
 
 (* preprocessing of equations *)
 
 (*rec_fn_opt records equations already noted for this function*)
 fun process_eqn thy (eq, rec_fn_opt) =
   let
     val (lhs, rhs) =
         if null (Term.add_vars eq []) then
             dest_eqn eq handle TERM _ => raise RecError "not a proper equation"
         else raise RecError "illegal schematic variable(s)";
 
     val (recfun, args) = strip_comb lhs;
     val (fname, ftype) = dest_Const recfun handle TERM _ =>
       raise RecError "function is not declared as constant in theory";
 
     val (ls_frees, rest)  = chop_prefix is_Free args;
     val (middle, rs_frees) = chop_suffix is_Free rest;
 
     val (constr, cargs_frees) =
       if null middle then raise RecError "constructor missing"
       else strip_comb (hd middle);
     val (cname, _) = dest_Const constr
       handle TERM _ => raise RecError "ill-formed constructor";
     val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
       handle Option.Option =>
       raise RecError "cannot determine datatype associated with function"
 
     val (ls, cargs, rs) = (map dest_Free ls_frees,
                            map dest_Free cargs_frees,
                            map dest_Free rs_frees)
       handle TERM _ => raise RecError "illegal argument in pattern";
     val lfrees = ls @ rs @ cargs;
 
     (*Constructor, frees to left of pattern, pattern variables,
       frees to right of pattern, rhs of equation, full original equation. *)
     val new_eqn = (cname, (rhs, cargs, eq))
 
   in
     if has_duplicates (op =) lfrees then
       raise RecError "repeated variable name in pattern"
     else if not (subset (op =) (Term.add_frees rhs [], lfrees)) then
       raise RecError "extra variables on rhs"
     else if length middle > 1 then
       raise RecError "more than one non-variable in pattern"
     else case rec_fn_opt of
         NONE => SOME (fname, ftype, ls, rs, con_info, [new_eqn])
       | SOME (fname', _, ls', rs', con_info': constructor_info, eqns) =>
           if AList.defined (op =) eqns cname then
             raise RecError "constructor already occurred as pattern"
           else if (ls <> ls') orelse (rs <> rs') then
             raise RecError "non-recursive arguments are inconsistent"
           else if #big_rec_name con_info <> #big_rec_name con_info' then
              raise RecError ("Mixed datatypes for function " ^ fname)
           else if fname <> fname' then
              raise RecError ("inconsistent functions for datatype " ^
                              #big_rec_name con_info)
           else SOME (fname, ftype, ls, rs, con_info, new_eqn::eqns)
   end
   handle RecError s => primrec_eq_err thy s eq;
 
 
 (*Instantiates a recursor equation with constructor arguments*)
 fun inst_recursor ((_ $ constr, rhs), cargs') =
     subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs;
 
 
 (*Convert a list of recursion equations into a recursor call*)
 fun process_fun thy (fname, ftype, ls, rs, con_info: constructor_info, eqns) =
   let
     val fconst = Const(fname, ftype)
     val fabs = list_comb (fconst, map Free ls @ [Bound 0] @ map Free rs)
     and {big_rec_name, constructors, rec_rewrites, ...} = con_info
 
     (*Replace X_rec(args,t) by fname(ls,t,rs) *)
     fun use_fabs (_ $ t) = subst_bound (t, fabs)
       | use_fabs t       = t
 
     val cnames         = map (#1 o dest_Const) constructors
     and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites
 
     fun absterm (Free x, body) = absfree x body
-      | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
+      | absterm (t, body) = Abs("rec", \<^Type>\<open>i\<close>, abstract_over (t, body))
 
     (*Translate rec equations into function arguments suitable for recursor.
       Missing cases are replaced by 0 and all cases are put into order.*)
     fun add_case ((cname, recursor_pair), cases) =
       let val (rhs, recursor_rhs, eq) =
             case AList.lookup (op =) eqns cname of
                 NONE => (warning ("no equation for constructor " ^ cname ^
                                   "\nin definition of function " ^ fname);
                          (\<^Const>\<open>zero\<close>, #2 recursor_pair, \<^Const>\<open>zero\<close>))
               | SOME (rhs, cargs', eq) =>
                     (rhs, inst_recursor (recursor_pair, cargs'), eq)
           val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
           val abs = List.foldr absterm rhs allowed_terms
       in
           if !Ind_Syntax.trace then
               writeln ("recursor_rhs = " ^
                        Syntax.string_of_term_global thy recursor_rhs ^
                        "\nabs = " ^ Syntax.string_of_term_global thy abs)
           else();
           if Logic.occs (fconst, abs) then
               primrec_eq_err thy
                    ("illegal recursive occurrences of " ^ fname)
                    eq
           else abs :: cases
       end
 
     val recursor = head_of (#1 (hd recursor_pairs))
 
     (** make definition **)
 
     (*the recursive argument*)
     val rec_arg =
       Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
-        Ind_Syntax.iT)
+        \<^Type>\<open>i\<close>)
 
     val def_tm = Logic.mk_equals
                     (subst_bound (rec_arg, fabs),
                      list_comb (recursor,
                                 List.foldr add_case [] (cnames ~~ recursor_pairs))
                      $ rec_arg)
 
   in
       if !Ind_Syntax.trace then
             writeln ("primrec def:\n" ^
                      Syntax.string_of_term_global thy def_tm)
       else();
       (Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def",
        def_tm)
   end;
 
 
 (* prepare functions needed for definitions *)
 
 fun primrec_i args thy =
   let
     val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
     val SOME (fname, ftype, ls, rs, con_info, eqns) =
       List.foldr (process_eqn thy) NONE eqn_terms;
     val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
 
     val ([def_thm], thy1) = thy
       |> Sign.add_path (Long_Name.base_name fname)
       |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)];
 
     val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info)
     val eqn_thms0 =
       eqn_terms |> map (fn t =>
         Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
           (fn {context = ctxt, ...} =>
             EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt @{thms refl} 1]));
   in
     thy1
     |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms0) ~~ eqn_atts)
     |-> (fn eqn_thms =>
       Global_Theory.add_thmss [((Binding.name "simps", eqn_thms), [Simplifier.simp_add])])
     |>> the_single
     ||> Sign.parent_path
   end;
 
 fun primrec args thy =
   primrec_i (map (fn ((name, s), srcs) =>
     ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs))
     args) thy;
 
 
 (* outer syntax *)
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>primrec\<close> "define primitive recursive functions on datatypes"
     (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
       >> (Toplevel.theory o (#2 oo (primrec o map (fn ((x, y), z) => ((x, z), y))))));
 
 end;
 
diff --git a/src/ZF/arith_data.ML b/src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML
+++ b/src/ZF/arith_data.ML
@@ -1,275 +1,272 @@
 (*  Title:      ZF/arith_data.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Arithmetic simplification: cancellation of common terms
 *)
 
 signature ARITH_DATA =
 sig
   (*the main outcome*)
   val nat_cancel: simproc list
   (*tools for use in similar applications*)
   val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
   val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
   val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
   (*debugging*)
   structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
   structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA
   structure DiffCancelNumeralsData : CANCEL_NUMERALS_DATA
 end;
 
 
 structure ArithData: ARITH_DATA =
 struct
 
-val iT = Ind_Syntax.iT;
-
 val zero = \<^Const>\<open>zero\<close>;
 val succ = \<^Const>\<open>succ\<close>;
 fun mk_succ t = succ $ t;
 val one = mk_succ zero;
 
 fun mk_plus (t, u) = \<^Const>\<open>Arith.add for t u\<close>;
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
   | mk_sum [t,u]     = mk_plus (t, u)
   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
 (* dest_sum *)
 
 fun dest_sum \<^Const_>\<open>zero\<close> = []
   | dest_sum \<^Const_>\<open>succ for t\<close> = one :: dest_sum t
   | dest_sum \<^Const_>\<open>Arith.add for t u\<close> = dest_sum t @ dest_sum u
   | dest_sum tm = [tm];
 
 (*Apply the given rewrite (if present) just once*)
 fun gen_trans_tac _ _ NONE = all_tac
   | gen_trans_tac ctxt th2 (SOME th) = ALLGOALS (resolve_tac ctxt [th RS th2]);
 
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =
-  if fastype_of t = iT then FOLogic.mk_eq(t,u)
-                       else FOLogic.mk_iff(t,u);
+  if fastype_of t = \<^Type>\<open>i\<close>
+  then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+  else \<^Const>\<open>IFOL.iff for t u\<close>;
 
 (*We remove equality assumptions because they confuse the simplifier and
   because only type-checking assumptions are necessary.*)
 fun is_eq_thm th =
     can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
 
 fun prove_conv name tacs ctxt prems (t,u) =
   if t aconv u then NONE
   else
   let val prems' = filter_out is_eq_thm prems
       val goal = Logic.list_implies (map Thm.prop_of prems',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
   in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
       handle ERROR msg =>
         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
   end;
 
 
 (*** Use CancelNumerals simproc without binary numerals,
      just for cancellation ***)
 
 fun mk_times (t, u) = \<^Const>\<open>Arith.mult for t u\<close>;
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin \<^const_name>\<open>Arith.mult\<close> iT;
-
-fun dest_prod t =
-      let val (t,u) = dest_times t
-      in  dest_prod t @ dest_prod u  end
-      handle TERM _ => [t];
+fun dest_prod tm =
+  let val (t,u) = \<^Const_fn>\<open>Arith.mult for t u => \<open>(t, u)\<close>\<close> tm
+  in  dest_prod t @ dest_prod u  end
+  handle TERM _ => [tm];
 
 (*Dummy version: the only arguments are 0 and 1*)
 fun mk_coeff (0, t) = zero
   | mk_coeff (1, t) = t
   | mk_coeff _       = raise TERM("mk_coeff", []);
 
 (*Dummy version: the "coefficient" is always 1.
   In the result, the factors are sorted terms*)
 fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t)));
 
 (*Find first coefficient-term THAT MATCHES u*)
 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   | find_first_coeff past u (t::terms) =
         let val (n,u') = dest_coeff t
         in  if u aconv u' then (n, rev past @ terms)
                           else find_first_coeff (t::past) u terms
         end
         handle TERM _ => find_first_coeff (t::past) u terms;
 
 
 (*Simplify #1*n and n*#1 to n*)
 val add_0s = [@{thm add_0_natify}, @{thm add_0_right_natify}];
 val add_succs = [@{thm add_succ}, @{thm add_succ_right}];
 val mult_1s = [@{thm mult_1_natify}, @{thm mult_1_right_natify}];
 val tc_rules = [@{thm natify_in_nat}, @{thm add_type}, @{thm diff_type}, @{thm mult_type}];
 val natifys = [@{thm natify_0}, @{thm natify_ident}, @{thm add_natify1}, @{thm add_natify2},
                @{thm diff_natify1}, @{thm diff_natify2}];
 
 (*Final simplification: cancel + and **)
 fun simplify_meta_eq rules ctxt =
   let val ctxt' =
     put_simpset FOL_ss ctxt
       delsimps @{thms iff_simps} (*these could erase the whole rule!*)
       addsimps rules
       |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}]
   in mk_meta_eq o simplify ctxt' end;
 
 val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}];
 
 structure CancelNumeralsCommon =
   struct
   val mk_sum            = (fn T:typ => mk_sum)
   val dest_sum          = dest_sum
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first_coeff  = find_first_coeff []
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac})
   val norm_ss2 =
     simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ mult_1s @ @{thms add_ac} @
       @{thms mult_ac} @ tc_rules @ natifys)
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
   val numeral_simp_ss =
     simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ tc_rules @ natifys)
   fun numeral_simp_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq  = simplify_meta_eq final_rules
   end;
 
 (** The functor argumnets are declared as separate structures
     so that they can be exported to ease debugging. **)
 
 structure EqCancelNumeralsData =
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "nateq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
   val dest_bal = FOLogic.dest_eq
   val bal_add1 = @{thm eq_add_iff [THEN iff_trans]}
   val bal_add2 = @{thm eq_add_iff [THEN iff_trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
   end;
 
 structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
 
 structure LessCancelNumeralsData =
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natless_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>Ordinal.lt for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
+  val dest_bal = \<^Const_fn>\<open>Ordinal.lt for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm less_add_iff [THEN iff_trans]}
   val bal_add2 = @{thm less_add_iff [THEN iff_trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
   end;
 
 structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
 
 structure DiffCancelNumeralsData =
   struct
   open CancelNumeralsCommon
   val prove_conv = prove_conv "natdiff_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>Arith.diff for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
+  val dest_bal = \<^Const_fn>\<open>Arith.diff for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm diff_add_eq [THEN trans]}
   val bal_add2 = @{thm diff_add_eq [THEN trans]}
   fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
   end;
 
 structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
 
 
 val nat_cancel =
  [Simplifier.make_simproc \<^context> "nateq_cancel_numerals"
    {lhss =
      [\<^term>\<open>l #+ m = n\<close>, \<^term>\<open>l = m #+ n\<close>,
       \<^term>\<open>l #* m = n\<close>, \<^term>\<open>l = m #* n\<close>,
       \<^term>\<open>succ(m) = n\<close>, \<^term>\<open>m = succ(n)\<close>],
     proc = K EqCancelNumerals.proc},
   Simplifier.make_simproc \<^context> "natless_cancel_numerals"
    {lhss =
      [\<^term>\<open>l #+ m < n\<close>, \<^term>\<open>l < m #+ n\<close>,
       \<^term>\<open>l #* m < n\<close>, \<^term>\<open>l < m #* n\<close>,
       \<^term>\<open>succ(m) < n\<close>, \<^term>\<open>m < succ(n)\<close>],
     proc = K LessCancelNumerals.proc},
   Simplifier.make_simproc \<^context> "natdiff_cancel_numerals"
    {lhss =
      [\<^term>\<open>(l #+ m) #- n\<close>, \<^term>\<open>l #- (m #+ n)\<close>,
       \<^term>\<open>(l #* m) #- n\<close>, \<^term>\<open>l #- (m #* n)\<close>,
       \<^term>\<open>succ(m) #- n\<close>, \<^term>\<open>m #- succ(n)\<close>],
     proc = K DiffCancelNumerals.proc}];
 
 end;
 
 val _ =
   Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
     ctxt addsimprocs ArithData.nat_cancel));
 
 
 (*examples:
 print_depth 22;
 set timing;
 set simp_trace;
 fun test s = (Goal s; by (Asm_simp_tac 1));
 
 test "x #+ y = x #+ z";
 test "y #+ x = x #+ z";
 test "x #+ y #+ z = x #+ z";
 test "y #+ (z #+ x) = z #+ x";
 test "x #+ y #+ z = (z #+ y) #+ (x #+ w)";
 test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)";
 
 test "x #+ succ(y) = x #+ z";
 test "x #+ succ(y) = succ(z #+ x)";
 test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)";
 
 test "(x #+ y) #- (x #+ z) = w";
 test "(y #+ x) #- (x #+ z) = dd";
 test "(x #+ y #+ z) #- (x #+ z) = dd";
 test "(y #+ (z #+ x)) #- (z #+ x) = dd";
 test "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd";
 test "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd";
 
 (*BAD occurrence of natify*)
 test "(x #+ succ(y)) #- (x #+ z) = dd";
 
 test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2";
 
 test "(x #+ succ(y)) #- (succ(z #+ x)) = dd";
 test "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd";
 
 (*use of typing information*)
 test "x : nat ==> x #+ y = x";
 test "x : nat --> x #+ y = x";
 test "x : nat ==> x #+ y < x";
 test "x : nat ==> x < y#+x";
 test "x : nat ==> x le succ(x)";
 
 (*fails: no typing information isn't visible*)
 test "x #+ y = x";
 
 test "x #+ y < x #+ z";
 test "y #+ x < x #+ z";
 test "x #+ y #+ z < x #+ z";
 test "y #+ z #+ x < x #+ z";
 test "y #+ (z #+ x) < z #+ x";
 test "x #+ y #+ z < (z #+ y) #+ (x #+ w)";
 test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)";
 
 test "x #+ succ(y) < x #+ z";
 test "x #+ succ(y) < succ(z #+ x)";
 test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)";
 
 test "x #+ succ(y) le succ(z #+ x)";
 *)
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,119 +1,117 @@
 (*  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 **)
 
-val iT = \<^Type>\<open>i\<close>;
-
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
-    FOLogic.all_const iT $
-      Abs("v", iT, FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
+    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));
 
-fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) t;
+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 FOLogic.oT) sprems
+    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) ---> iT
+        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 = iT)
+      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;
 
diff --git a/src/ZF/int_arith.ML b/src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML
+++ b/src/ZF/int_arith.ML
@@ -1,327 +1,325 @@
 (*  Title:      ZF/int_arith.ML
     Author:     Larry Paulson
 
 Simprocs for linear arithmetic.
 *)
 
 signature INT_NUMERAL_SIMPROCS =
 sig
   val cancel_numerals: simproc list
   val combine_numerals: simproc
   val combine_numerals_prod: simproc
 end
 
 structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =
 struct
 
 (* abstract syntax operations *)
 
 fun mk_bit 0 = \<^term>\<open>0\<close>
   | mk_bit 1 = \<^term>\<open>succ(0)\<close>
   | mk_bit _ = raise TERM ("mk_bit", []);
 
 fun dest_bit \<^term>\<open>0\<close> = 0
   | dest_bit \<^term>\<open>succ(0)\<close> = 1
   | dest_bit t = raise TERM ("dest_bit", [t]);
 
 fun mk_bin i =
   let
     fun term_of [] = \<^term>\<open>Pls\<close>
       | term_of [~1] = \<^term>\<open>Min\<close>
       | term_of (b :: bs) = \<^term>\<open>Bit\<close> $ term_of bs $ mk_bit b;
   in term_of (Numeral_Syntax.make_binary i) end;
 
 fun dest_bin tm =
   let
     fun bin_of \<^term>\<open>Pls\<close> = []
       | bin_of \<^term>\<open>Min\<close> = [~1]
       | bin_of (\<^term>\<open>Bit\<close> $ bs $ b) = dest_bit b :: bin_of bs
       | bin_of _ = raise TERM ("dest_bin", [tm]);
   in Numeral_Syntax.dest_binary (bin_of tm) end;
 
 
 (*Utilities*)
 
 fun mk_numeral i = \<^Const>\<open>integ_of\<close> $ mk_bin i;
 
 fun dest_numeral \<^Const_>\<open>integ_of for w\<close> = dest_bin w
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
 fun find_first_numeral past (t::terms) =
         ((dest_numeral t, rev past @ terms)
          handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_numeral 0;
 fun mk_plus (t, u) = \<^Const>\<open>zadd for t u\<close>;
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
   | mk_sum [t,u]     = mk_plus (t, u)
   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
 (*this version ALWAYS includes a trailing zero*)
 fun long_mk_sum []        = zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
 (*decompose additions AND subtractions as a sum*)
 fun dest_summing (pos, \<^Const_>\<open>zadd for t u\<close>, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
   | dest_summing (pos, \<^Const_>\<open>zdiff for t u\<close>, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
         if pos then t::ts else \<^Const>\<open>zminus for t\<close> :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);
 
 val one = mk_numeral 1;
 fun mk_times (t, u) = \<^Const>\<open>zmult for t u\<close>;
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin \<^const_name>\<open>zmult\<close> \<^typ>\<open>i\<close>;
-
-fun dest_prod t =
-      let val (t,u) = dest_times t
-      in  dest_prod t @ dest_prod u  end
-      handle TERM _ => [t];
+fun dest_prod tm =
+  let val (t,u) = \<^Const_fn>\<open>zmult for t u => \<open>(t, u)\<close>\<close> tm
+  in  dest_prod t @ dest_prod u  end
+  handle TERM _ => [tm];
 
 (*DON'T do the obvious simplifications; that would create special cases*)
 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
 fun dest_coeff sign \<^Const_>\<open>zminus for t\<close> = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort Term_Ord.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
                           handle TERM _ => (1, ts)
     in (sign*n, mk_prod ts') end;
 
 (*Find first coefficient-term THAT MATCHES u*)
 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   | find_first_coeff past u (t::terms) =
         let val (n,u') = dest_coeff 1 t
         in  if u aconv u' then (n, rev past @ terms)
                           else find_first_coeff (t::past) u terms
         end
         handle TERM _ => find_first_coeff (t::past) u terms;
 
 
 (*Simplify #1*n and n*#1 to n*)
 val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}];
 
 val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify},
                @{thm zmult_minus1}, @{thm zmult_minus1_right}];
 
 val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int},
                 @{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ 
                @{thms bin.intros};
 val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2},
                @{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2},
                @{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}];
 
 (*To perform binary arithmetic*)
 val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps};
 
 (*To evaluate binary negations of coefficients*)
 val zminus_simps = @{thms NCons_simps} @
                    [@{thm integ_of_minus} RS @{thm sym},
                     @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
                     @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
 
 (*To let us treat subtraction as addition*)
 val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
 
 (*push the unary minus down*)
 val int_minus_mult_eq_1_to_2 = @{lemma "$- w $* z = w $* $- z" by simp};
 
 (*to extract again any uncancelled minuses*)
 val int_minus_from_mult_simps =
     [@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}];
 
 (*combine unary minus with numeric literals, however nested within a product*)
 val int_mult_minus_simps =
     [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
 
 structure CancelNumeralsCommon =
   struct
   val mk_sum = (fn _ : typ => mk_sum)
   val dest_sum = dest_sum
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff 1
   val find_first_coeff = find_first_coeff []
   fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans}
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac})
   val norm_ss2 =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps bin_simps @ int_mult_minus_simps @ intifys)
   val norm_ss3 =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt))
 
   val numeral_simp_ss =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps add_0s @ bin_simps @ tc_rules @ intifys)
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
     THEN ALLGOALS (asm_simp_tac ctxt)
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
   val dest_bal = FOLogic.dest_eq
   val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans}
 );
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>zless for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<close>
+  val dest_bal = \<^Const_fn>\<open>zless for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
 );
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   fun mk_bal (t, u) = \<^Const>\<open>zle for t u\<close>
-  val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zle\<close> \<^typ>\<open>i\<close>
+  val dest_bal = \<^Const_fn>\<open>zle for t u => \<open>(t, u)\<close>\<close>
   val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
   val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
 );
 
 val cancel_numerals =
  [Simplifier.make_simproc \<^context> "inteq_cancel_numerals"
    {lhss =
      [\<^term>\<open>l $+ m = n\<close>, \<^term>\<open>l = m $+ n\<close>,
       \<^term>\<open>l $- m = n\<close>, \<^term>\<open>l = m $- n\<close>,
       \<^term>\<open>l $* m = n\<close>, \<^term>\<open>l = m $* n\<close>],
     proc = K EqCancelNumerals.proc},
   Simplifier.make_simproc \<^context> "intless_cancel_numerals"
    {lhss =
      [\<^term>\<open>l $+ m $< n\<close>, \<^term>\<open>l $< m $+ n\<close>,
       \<^term>\<open>l $- m $< n\<close>, \<^term>\<open>l $< m $- n\<close>,
       \<^term>\<open>l $* m $< n\<close>, \<^term>\<open>l $< m $* n\<close>],
     proc = K LessCancelNumerals.proc},
   Simplifier.make_simproc \<^context> "intle_cancel_numerals"
    {lhss =
      [\<^term>\<open>l $+ m $\<le> n\<close>, \<^term>\<open>l $\<le> m $+ n\<close>,
       \<^term>\<open>l $- m $\<le> n\<close>, \<^term>\<open>l $\<le> m $- n\<close>,
       \<^term>\<open>l $* m $\<le> n\<close>, \<^term>\<open>l $\<le> m $* n\<close>],
     proc = K LeCancelNumerals.proc}];
 
 
 (*version without the hyps argument*)
 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
 
 structure CombineNumeralsData =
   struct
   type coeff = int
   val iszero = (fn x => x = 0)
   val add = op + 
   val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   val dest_sum = dest_sum
   val mk_coeff = mk_coeff
   val dest_coeff = dest_coeff 1
   val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
   val prove_conv = prove_conv_nohyps "int_combine_numerals"
   fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys)
   val norm_ss2 =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps bin_simps @ int_mult_minus_simps @ intifys)
   val norm_ss3 =
     simpset_of (put_simpset ZF_ss \<^context>
       addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt))
 
   val numeral_simp_ss =
     simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ bin_simps @ tc_rules @ intifys)
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
 val combine_numerals =
   Simplifier.make_simproc \<^context> "int_combine_numerals"
     {lhss = [\<^term>\<open>i $+ j\<close>, \<^term>\<open>i $- j\<close>],
      proc = K CombineNumerals.proc};
 
 
 
 (** Constant folding for integer multiplication **)
 
 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   the "sum" of #3, x, #4; the literals are then multiplied*)
 
 
 structure CombineNumeralsProdData =
 struct
   type coeff = int
   val iszero = (fn x => x = 0)
   val add = op *
   val mk_sum = (fn _ : typ => mk_prod)
   val dest_sum = dest_prod
   fun mk_coeff(k,t) =
     if t = one then mk_numeral k
     else raise TERM("mk_coeff", [])
   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
   val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
   fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss \<^context> addsimps mult_1s @ diff_simps @ zminus_simps)
   val norm_ss2 =
     simpset_of (put_simpset ZF_ss \<^context> addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
     bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
 
   val numeral_simp_ss =
     simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ tc_rules @ intifys)
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
 end;
 
 
 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
 
 val combine_numerals_prod =
   Simplifier.make_simproc \<^context> "int_combine_numerals_prod"
    {lhss = [\<^term>\<open>i $* j\<close>], proc = K CombineNumeralsProd.proc};
 
 end;
 
 val _ =
   Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
     ctxt addsimprocs
       (Int_Numeral_Simprocs.cancel_numerals @
        [Int_Numeral_Simprocs.combine_numerals,
         Int_Numeral_Simprocs.combine_numerals_prod])));