diff --git a/src/ZF/Inductive.thy b/src/ZF/Inductive.thy
--- a/src/ZF/Inductive.thy
+++ b/src/ZF/Inductive.thy
@@ -1,132 +1,132 @@
 (*  Title:      ZF/Inductive.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Inductive definitions use least fixedpoints with standard products and sums
 Coinductive definitions use greatest fixedpoints with Quine products and sums
 
 Sums are used only for mutual recursion;
 Products are used only to derive "streamlined" induction rules for relations
 *)
 
 section\<open>Inductive and Coinductive Definitions\<close>
 
 theory Inductive
 imports Fixedpt QPair Nat
 keywords
   "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
     "elimination" "induction" "case_eqns" "recursor_eqns" :: quasi_command
 begin
 
 lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
   by blast
 
 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
   by simp
 
 lemma refl_thin: "!!P. a = a ==> P ==> P" .
 
 ML_file \<open>ind_syntax.ML\<close>
 ML_file \<open>Tools/ind_cases.ML\<close>
 ML_file \<open>Tools/cartprod.ML\<close>
 ML_file \<open>Tools/inductive_package.ML\<close>
 ML_file \<open>Tools/induct_tacs.ML\<close>
 ML_file \<open>Tools/primrec_package.ML\<close>
 
 ML \<open>
 structure Lfp =
   struct
-  val oper      = \<^const>\<open>lfp\<close>
-  val bnd_mono  = \<^const>\<open>bnd_mono\<close>
+  val oper      = \<^Const>\<open>lfp\<close>
+  val bnd_mono  = \<^Const>\<open>bnd_mono\<close>
   val bnd_monoI = @{thm bnd_monoI}
   val subs      = @{thm def_lfp_subset}
   val Tarski    = @{thm def_lfp_unfold}
   val induct    = @{thm def_induct}
   end;
 
 structure Standard_Prod =
   struct
-  val sigma     = \<^const>\<open>Sigma\<close>
-  val pair      = \<^const>\<open>Pair\<close>
+  val sigma     = \<^Const>\<open>Sigma\<close>
+  val pair      = \<^Const>\<open>Pair\<close>
   val split_name = \<^const_name>\<open>split\<close>
   val pair_iff  = @{thm Pair_iff}
   val split_eq  = @{thm split}
   val fsplitI   = @{thm splitI}
   val fsplitD   = @{thm splitD}
   val fsplitE   = @{thm splitE}
   end;
 
 structure Standard_CP = CartProd_Fun (Standard_Prod);
 
 structure Standard_Sum =
   struct
-  val sum       = \<^const>\<open>sum\<close>
-  val inl       = \<^const>\<open>Inl\<close>
-  val inr       = \<^const>\<open>Inr\<close>
-  val elim      = \<^const>\<open>case\<close>
+  val sum       = \<^Const>\<open>sum\<close>
+  val inl       = \<^Const>\<open>Inl\<close>
+  val inr       = \<^Const>\<open>Inr\<close>
+  val elim      = \<^Const>\<open>case\<close>
   val case_inl  = @{thm case_Inl}
   val case_inr  = @{thm case_Inr}
   val inl_iff   = @{thm Inl_iff}
   val inr_iff   = @{thm Inr_iff}
   val distinct  = @{thm Inl_Inr_iff}
   val distinct' = @{thm Inr_Inl_iff}
   val free_SEs  = Ind_Syntax.mk_free_SEs
             [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
   end;
 
 
 structure Ind_Package =
     Add_inductive_def_Fun
       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
        and Su=Standard_Sum val coind = false);
 
 
 structure Gfp =
   struct
-  val oper      = \<^const>\<open>gfp\<close>
-  val bnd_mono  = \<^const>\<open>bnd_mono\<close>
+  val oper      = \<^Const>\<open>gfp\<close>
+  val bnd_mono  = \<^Const>\<open>bnd_mono\<close>
   val bnd_monoI = @{thm bnd_monoI}
   val subs      = @{thm def_gfp_subset}
   val Tarski    = @{thm def_gfp_unfold}
   val induct    = @{thm def_Collect_coinduct}
   end;
 
 structure Quine_Prod =
   struct
-  val sigma     = \<^const>\<open>QSigma\<close>
-  val pair      = \<^const>\<open>QPair\<close>
+  val sigma     = \<^Const>\<open>QSigma\<close>
+  val pair      = \<^Const>\<open>QPair\<close>
   val split_name = \<^const_name>\<open>qsplit\<close>
   val pair_iff  = @{thm QPair_iff}
   val split_eq  = @{thm qsplit}
   val fsplitI   = @{thm qsplitI}
   val fsplitD   = @{thm qsplitD}
   val fsplitE   = @{thm qsplitE}
   end;
 
 structure Quine_CP = CartProd_Fun (Quine_Prod);
 
 structure Quine_Sum =
   struct
-  val sum       = \<^const>\<open>qsum\<close>
-  val inl       = \<^const>\<open>QInl\<close>
-  val inr       = \<^const>\<open>QInr\<close>
-  val elim      = \<^const>\<open>qcase\<close>
+  val sum       = \<^Const>\<open>qsum\<close>
+  val inl       = \<^Const>\<open>QInl\<close>
+  val inr       = \<^Const>\<open>QInr\<close>
+  val elim      = \<^Const>\<open>qcase\<close>
   val case_inl  = @{thm qcase_QInl}
   val case_inr  = @{thm qcase_QInr}
   val inl_iff   = @{thm QInl_iff}
   val inr_iff   = @{thm QInr_iff}
   val distinct  = @{thm QInl_QInr_iff}
   val distinct' = @{thm QInr_QInl_iff}
   val free_SEs  = Ind_Syntax.mk_free_SEs
             [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
   end;
 
 
 structure CoInd_Package =
   Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
     and Su=Quine_Sum val coind = true);
 
 \<close>
 
 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 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>
+  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)
           | call_f (free,args) =
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
                             \<^typ>\<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", \<^typ>\<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
 
   (*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> $
+         \<^Const>\<open>Univ.Vrecursor\<close> $
            absfree ("rec", \<^typ>\<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
       |> 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,611 +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))
     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);
+    | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, 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)
         (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));
 
   (*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)
+                             (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 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)
            val qconcl =
              List.foldr FOLogic.mk_all
-               (FOLogic.imp $
-                (\<^const>\<open>mem\<close> $ elem_tuple $ rec_tm)
+               (FOLogic.imp $ \<^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,
             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\<close> $ Bound 0 $ rec_tm) $
-                          (pred $ Bound 0);
+         FOLogic.imp $ \<^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,
                  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)
        |> 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)
       #> 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/ind_syntax.ML b/src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML
+++ b/src/ZF/ind_syntax.ML
@@ -1,121 +1,119 @@
 (*  Title:      ZF/ind_syntax.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Abstract Syntax functions for Inductive Definitions.
 *)
 
 structure Ind_Syntax =
 struct
 
 (*Print tracing messages during processing of "inductive" theory sections*)
 val trace = Unsynchronized.ref false;
 
 fun traceIt msg thy t =
   if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
   else t;
 
 
 (** Abstract syntax definitions for ZF **)
 
 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\<close> $ Bound 0 $ A) $
-                   Term.betapply(P, Bound 0));
+      Abs("v", iT, FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
 
-fun mk_Collect (a, D, t) = \<^const>\<open>Collect\<close> $ D $ absfree (a, iT) t;
+fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) 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
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT
                 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))
+            (\<^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\<close> $ t1 $ t2;
+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)
   in  case filter is_ind (args @ cs) of
-         [] => \<^const>\<open>zero\<close>
+         [] => \<^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,327 @@
 (*  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 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;
 val mk_plus = FOLogic.mk_binop \<^const_name>\<open>zadd\<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\<close> $ 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;
 val mk_times = FOLogic.mk_binop \<^const_name>\<open>zmult\<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];
 
 (*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"
   val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>zless\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<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"
   val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>zle\<close>
   val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zle\<close> \<^typ>\<open>i\<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])));