diff --git a/src/FOL/IFOL.thy b/src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy
+++ b/src/FOL/IFOL.thy
@@ -1,906 +1,906 @@
 (*  Title:      FOL/IFOL.thy
     Author:     Lawrence C Paulson and Markus Wenzel
 *)
 
 section \<open>Intuitionistic first-order logic\<close>
 
 theory IFOL
   imports Pure
   abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Provers/splitter.ML\<close>
 ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
 ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
 ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
 ML_file \<open>~~/src/Tools/intuitionistic.ML\<close>
 ML_file \<open>~~/src/Tools/project_rule.ML\<close>
 ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
 
 
 subsection \<open>Syntax and axiomatic basis\<close>
 
 setup Pure_Thy.old_appl_syntax_setup
 setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close>
 
 class "term"
 default_sort \<open>term\<close>
 
 typedecl o
 
 judgment
   Trueprop :: \<open>o \<Rightarrow> prop\<close>  (\<open>(_)\<close> 5)
 
 
 subsubsection \<open>Equality\<close>
 
 axiomatization
   eq :: \<open>['a, 'a] \<Rightarrow> o\<close>  (infixl \<open>=\<close> 50)
 where
   refl: \<open>a = a\<close> and
   subst: \<open>a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)\<close>
 
 
 subsubsection \<open>Propositional logic\<close>
 
 axiomatization
   False :: \<open>o\<close> and
   conj :: \<open>[o, o] => o\<close>  (infixr \<open>\<and>\<close> 35) and
   disj :: \<open>[o, o] => o\<close>  (infixr \<open>\<or>\<close> 30) and
   imp :: \<open>[o, o] => o\<close>  (infixr \<open>\<longrightarrow>\<close> 25)
 where
   conjI: \<open>\<lbrakk>P;  Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close> and
   conjunct1: \<open>P \<and> Q \<Longrightarrow> P\<close> and
   conjunct2: \<open>P \<and> Q \<Longrightarrow> Q\<close> and
 
   disjI1: \<open>P \<Longrightarrow> P \<or> Q\<close> and
   disjI2: \<open>Q \<Longrightarrow> P \<or> Q\<close> and
   disjE: \<open>\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close> and
 
   impI: \<open>(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q\<close> and
   mp: \<open>\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q\<close> and
 
   FalseE: \<open>False \<Longrightarrow> P\<close>
 
 
 subsubsection \<open>Quantifiers\<close>
 
 axiomatization
   All :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close>  (binder \<open>\<forall>\<close> 10) and
   Ex :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close>  (binder \<open>\<exists>\<close> 10)
 where
   allI: \<open>(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))\<close> and
   spec: \<open>(\<forall>x. P(x)) \<Longrightarrow> P(x)\<close> and
   exI: \<open>P(x) \<Longrightarrow> (\<exists>x. P(x))\<close> and
   exE: \<open>\<lbrakk>\<exists>x. P(x); \<And>x. P(x) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close>
 
 
 subsubsection \<open>Definitions\<close>
 
 definition \<open>True \<equiv> False \<longrightarrow> False\<close>
 
 definition Not (\<open>\<not> _\<close> [40] 40)
   where not_def: \<open>\<not> P \<equiv> P \<longrightarrow> False\<close>
 
 definition iff  (infixr \<open>\<longleftrightarrow>\<close> 25)
   where \<open>P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)\<close>
 
 definition Uniq :: "('a \<Rightarrow> o) \<Rightarrow> o"
   where \<open>Uniq(P) \<equiv> (\<forall>x y. P(x) \<longrightarrow> P(y) \<longrightarrow> y = x)\<close>
 
 definition Ex1 :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close>  (binder \<open>\<exists>!\<close> 10)
   where ex1_def: \<open>\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)\<close>
 
 axiomatization where  \<comment> \<open>Reflection, admissible\<close>
   eq_reflection: \<open>(x = y) \<Longrightarrow> (x \<equiv> y)\<close> and
   iff_reflection: \<open>(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)\<close>
 
 abbreviation not_equal :: \<open>['a, 'a] \<Rightarrow> o\<close>  (infixl \<open>\<noteq>\<close> 50)
   where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
 
 syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o"  ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
 subsubsection \<open>Old-style ASCII syntax\<close>
 
 notation (ASCII)
   not_equal  (infixl \<open>~=\<close> 50) and
   Not  (\<open>~ _\<close> [40] 40) and
   conj  (infixr \<open>&\<close> 35) and
   disj  (infixr \<open>|\<close> 30) and
   All  (binder \<open>ALL \<close> 10) and
   Ex  (binder \<open>EX \<close> 10) and
   Ex1  (binder \<open>EX! \<close> 10) and
   imp  (infixr \<open>-->\<close> 25) and
   iff  (infixr \<open><->\<close> 25)
 
 
 subsection \<open>Lemmas and proof tools\<close>
 
 lemmas strip = impI allI
 
 lemma TrueI: \<open>True\<close>
   unfolding True_def by (rule impI)
 
 
 subsubsection \<open>Sequent-style elimination rules for \<open>\<and>\<close> \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close>\<close>
 
 lemma conjE:
   assumes major: \<open>P \<and> Q\<close>
     and r: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
 proof (rule r)
   show "P"
     by (rule major [THEN conjunct1])
   show "Q"
     by (rule major [THEN conjunct2])
 qed
 
 lemma impE:
   assumes major: \<open>P \<longrightarrow> Q\<close>
     and \<open>P\<close>
   and r: \<open>Q \<Longrightarrow> R\<close>
   shows \<open>R\<close>
 proof (rule r)
   show "Q"
     by (rule mp [OF major \<open>P\<close>])
 qed
 
 lemma allE:
   assumes major: \<open>\<forall>x. P(x)\<close>
     and r: \<open>P(x) \<Longrightarrow> R\<close>
   shows \<open>R\<close>
 proof (rule r)
   show "P(x)"
     by (rule major [THEN spec])
 qed
 
 text \<open>Duplicates the quantifier; for use with \<^ML>\<open>eresolve_tac\<close>.\<close>
 lemma all_dupE:
   assumes major: \<open>\<forall>x. P(x)\<close>
     and r: \<open>\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
 proof (rule r)
   show "P(x)"
     by (rule major [THEN spec])
 qed (rule major)
 
 
 
 subsubsection \<open>Negation rules, which translate between \<open>\<not> P\<close> and \<open>P \<longrightarrow> False\<close>\<close>
 
 lemma notI: \<open>(P \<Longrightarrow> False) \<Longrightarrow> \<not> P\<close>
   unfolding not_def by (erule impI)
 
 lemma notE: \<open>\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R\<close>
   unfolding not_def by (erule mp [THEN FalseE])
 
 lemma rev_notE: \<open>\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R\<close>
   by (erule notE)
 
 text \<open>This is useful with the special implication rules for each kind of \<open>P\<close>.\<close>
 lemma not_to_imp:
   assumes \<open>\<not> P\<close>
     and r: \<open>P \<longrightarrow> False \<Longrightarrow> Q\<close>
   shows \<open>Q\<close>
   apply (rule r)
   apply (rule impI)
   apply (erule notE [OF \<open>\<not> P\<close>])
   done
 
 text \<open>
   For substitution into an assumption \<open>P\<close>, reduce \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, substitute into this implication, then apply \<open>impI\<close> to
   move \<open>P\<close> back into the assumptions.
 \<close>
 lemma rev_mp: \<open>\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q\<close>
   by (erule mp)
 
 text \<open>Contrapositive of an inference rule.\<close>
 lemma contrapos:
   assumes major: \<open>\<not> Q\<close>
     and minor: \<open>P \<Longrightarrow> Q\<close>
   shows \<open>\<not> P\<close>
   apply (rule major [THEN notE, THEN notI])
   apply (erule minor)
   done
 
 
 subsubsection \<open>Modus Ponens Tactics\<close>
 
 text \<open>
   Finds \<open>P \<longrightarrow> Q\<close> and P in the assumptions, replaces implication by
   \<open>Q\<close>.
 \<close>
 ML \<open>
   fun mp_tac ctxt i =
     eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i;
   fun eq_mp_tac ctxt i =
     eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i;
 \<close>
 
 
 subsection \<open>If-and-only-if\<close>
 
 lemma iffI: \<open>\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q\<close>
   unfolding iff_def
   by (rule conjI; erule impI)
 
 lemma iffE:
   assumes major: \<open>P \<longleftrightarrow> Q\<close>
     and r: \<open>\<lbrakk>P \<longrightarrow> Q; Q \<longrightarrow> P\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   using major
   unfolding iff_def
   apply (rule conjE)
   apply (erule r)
   apply assumption
   done
 
 
 subsubsection \<open>Destruct rules for \<open>\<longleftrightarrow>\<close> similar to Modus Ponens\<close>
 
 lemma iffD1: \<open>\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q\<close>
   unfolding iff_def
   apply (erule conjunct1 [THEN mp])
   apply assumption
   done
 
 lemma iffD2: \<open>\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P\<close>
   unfolding iff_def
   apply (erule conjunct2 [THEN mp])
   apply assumption
   done
 
 lemma rev_iffD1: \<open>\<lbrakk>P; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> Q\<close>
   apply (erule iffD1)
   apply assumption
   done
 
 lemma rev_iffD2: \<open>\<lbrakk>Q; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> P\<close>
   apply (erule iffD2)
   apply assumption
   done
 
 lemma iff_refl: \<open>P \<longleftrightarrow> P\<close>
   by (rule iffI)
 
 lemma iff_sym: \<open>Q \<longleftrightarrow> P \<Longrightarrow> P \<longleftrightarrow> Q\<close>
   apply (erule iffE)
   apply (rule iffI)
   apply (assumption | erule mp)+
   done
 
 lemma iff_trans: \<open>\<lbrakk>P \<longleftrightarrow> Q; Q \<longleftrightarrow> R\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> R\<close>
   apply (rule iffI)
   apply (assumption | erule iffE | erule (1) notE impE)+
   done
 
 
 subsection \<open>Unique existence\<close>
 
 text \<open>
   NOTE THAT the following 2 quantifications:
 
     \<^item> \<open>\<exists>!x\<close> such that [\<open>\<exists>!y\<close> such that P(x,y)]   (sequential)
     \<^item> \<open>\<exists>!x,y\<close> such that P(x,y)                   (simultaneous)
 
   do NOT mean the same thing. The parser treats \<open>\<exists>!x y.P(x,y)\<close> as sequential.
 \<close>
 
 lemma ex1I: \<open>P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)\<close>
   unfolding ex1_def
   apply (assumption | rule exI conjI allI impI)+
   done
 
 text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
 lemma ex_ex1I: \<open>\<exists>x. P(x) \<Longrightarrow> (\<And>x y. \<lbrakk>P(x); P(y)\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> \<exists>!x. P(x)\<close>
   apply (erule exE)
   apply (rule ex1I)
    apply assumption
   apply assumption
   done
 
 lemma ex1E: \<open>\<exists>! x. P(x) \<Longrightarrow> (\<And>x. \<lbrakk>P(x); \<forall>y. P(y) \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R\<close>
   unfolding ex1_def
   apply (assumption | erule exE conjE)+
   done
 
 
 subsubsection \<open>\<open>\<longleftrightarrow>\<close> congruence rules for simplification\<close>
 
 text \<open>Use \<open>iffE\<close> on a premise. For \<open>conj_cong\<close>, \<open>imp_cong\<close>, \<open>all_cong\<close>, \<open>ex_cong\<close>.\<close>
 ML \<open>
   fun iff_tac ctxt prems i =
     resolve_tac ctxt (prems RL @{thms iffE}) i THEN
     REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i);
 \<close>
 
 method_setup iff =
   \<open>Attrib.thms >>
     (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
 
 lemma conj_cong:
   assumes \<open>P \<longleftrightarrow> P'\<close>
     and \<open>P' \<Longrightarrow> Q \<longleftrightarrow> Q'\<close>
   shows \<open>(P \<and> Q) \<longleftrightarrow> (P' \<and> Q')\<close>
   apply (insert assms)
   apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 text \<open>Reversed congruence rule!  Used in ZF/Order.\<close>
 lemma conj_cong2:
   assumes \<open>P \<longleftrightarrow> P'\<close>
     and \<open>P' \<Longrightarrow> Q \<longleftrightarrow> Q'\<close>
   shows \<open>(Q \<and> P) \<longleftrightarrow> (Q' \<and> P')\<close>
   apply (insert assms)
   apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 lemma disj_cong:
   assumes \<open>P \<longleftrightarrow> P'\<close> and \<open>Q \<longleftrightarrow> Q'\<close>
   shows \<open>(P \<or> Q) \<longleftrightarrow> (P' \<or> Q')\<close>
   apply (insert assms)
   apply (erule iffE disjE disjI1 disjI2 |
     assumption | rule iffI | erule (1) notE impE)+
   done
 
 lemma imp_cong:
   assumes \<open>P \<longleftrightarrow> P'\<close>
     and \<open>P' \<Longrightarrow> Q \<longleftrightarrow> Q'\<close>
   shows \<open>(P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')\<close>
   apply (insert assms)
   apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
   done
 
 lemma iff_cong: \<open>\<lbrakk>P \<longleftrightarrow> P'; Q \<longleftrightarrow> Q'\<rbrakk> \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P' \<longleftrightarrow> Q')\<close>
   apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
   done
 
 lemma not_cong: \<open>P \<longleftrightarrow> P' \<Longrightarrow> \<not> P \<longleftrightarrow> \<not> P'\<close>
   apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
   done
 
 lemma all_cong:
   assumes \<open>\<And>x. P(x) \<longleftrightarrow> Q(x)\<close>
   shows \<open>(\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close>
   apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
   done
 
 lemma ex_cong:
   assumes \<open>\<And>x. P(x) \<longleftrightarrow> Q(x)\<close>
   shows \<open>(\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close>
   apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
   done
 
 lemma ex1_cong:
   assumes \<open>\<And>x. P(x) \<longleftrightarrow> Q(x)\<close>
   shows \<open>(\<exists>!x. P(x)) \<longleftrightarrow> (\<exists>!x. Q(x))\<close>
   apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
   done
 
 
 subsection \<open>Equality rules\<close>
 
 lemma sym: \<open>a = b \<Longrightarrow> b = a\<close>
   apply (erule subst)
   apply (rule refl)
   done
 
 lemma trans: \<open>\<lbrakk>a = b; b = c\<rbrakk> \<Longrightarrow> a = c\<close>
   apply (erule subst, assumption)
   done
 
 lemma not_sym: \<open>b \<noteq> a \<Longrightarrow> a \<noteq> b\<close>
   apply (erule contrapos)
   apply (erule sym)
   done
 
 text \<open>
   Two theorems for rewriting only one instance of a definition:
   the first for definitions of formulae and the second for terms.
 \<close>
 
 lemma def_imp_iff: \<open>(A \<equiv> B) \<Longrightarrow> A \<longleftrightarrow> B\<close>
   apply unfold
   apply (rule iff_refl)
   done
 
 lemma meta_eq_to_obj_eq: \<open>(A \<equiv> B) \<Longrightarrow> A = B\<close>
   apply unfold
   apply (rule refl)
   done
 
 lemma meta_eq_to_iff: \<open>x \<equiv> y \<Longrightarrow> x \<longleftrightarrow> y\<close>
   by unfold (rule iff_refl)
 
 text \<open>Substitution.\<close>
 lemma ssubst: \<open>\<lbrakk>b = a; P(a)\<rbrakk> \<Longrightarrow> P(b)\<close>
   apply (drule sym)
   apply (erule (1) subst)
   done
 
 text \<open>A special case of \<open>ex1E\<close> that would otherwise need quantifier
   expansion.\<close>
 lemma ex1_equalsE: \<open>\<lbrakk>\<exists>!x. P(x); P(a); P(b)\<rbrakk> \<Longrightarrow> a = b\<close>
   apply (erule ex1E)
   apply (rule trans)
    apply (rule_tac [2] sym)
    apply (assumption | erule spec [THEN mp])+
   done
 
 
 subsection \<open>Simplifications of assumed implications\<close>
 
 text \<open>
   Roy Dyckhoff has proved that \<open>conj_impE\<close>, \<open>disj_impE\<close>, and
   \<open>imp_impE\<close> used with \<^ML>\<open>mp_tac\<close> (restricted to atomic formulae) is
   COMPLETE for intuitionistic propositional logic.
 
   See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   (preprint, University of St Andrews, 1991).
 \<close>
 
 lemma conj_impE:
   assumes major: \<open>(P \<and> Q) \<longrightarrow> S\<close>
     and r: \<open>P \<longrightarrow> (Q \<longrightarrow> S) \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   by (assumption | rule conjI impI major [THEN mp] r)+
 
 lemma disj_impE:
   assumes major: \<open>(P \<or> Q) \<longrightarrow> S\<close>
     and r: \<open>\<lbrakk>P \<longrightarrow> S; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+
 
 text \<open>Simplifies the implication.  Classical version is stronger.
   Still UNSAFE since Q must be provable -- backtracking needed.\<close>
 lemma imp_impE:
   assumes major: \<open>(P \<longrightarrow> Q) \<longrightarrow> S\<close>
     and r1: \<open>\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q\<close>
     and r2: \<open>S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   by (assumption | rule impI major [THEN mp] r1 r2)+
 
 text \<open>Simplifies the implication.  Classical version is stronger.
   Still UNSAFE since ~P must be provable -- backtracking needed.\<close>
 lemma not_impE: \<open>\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R\<close>
   apply (drule mp)
    apply (rule notI | assumption)+
   done
 
 text \<open>Simplifies the implication. UNSAFE.\<close>
 lemma iff_impE:
   assumes major: \<open>(P \<longleftrightarrow> Q) \<longrightarrow> S\<close>
     and r1: \<open>\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q\<close>
     and r2: \<open>\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P\<close>
     and r3: \<open>S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   by (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
 
 text \<open>What if \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close> is an assumption?
   UNSAFE.\<close>
 lemma all_impE:
   assumes major: \<open>(\<forall>x. P(x)) \<longrightarrow> S\<close>
     and r1: \<open>\<And>x. P(x)\<close>
     and r2: \<open>S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   by (rule allI impI major [THEN mp] r1 r2)+
 
 text \<open>
   Unsafe: \<open>\<exists>x. P(x)) \<longrightarrow> S\<close> is equivalent
   to \<open>\<forall>x. P(x) \<longrightarrow> S\<close>.\<close>
 lemma ex_impE:
   assumes major: \<open>(\<exists>x. P(x)) \<longrightarrow> S\<close>
     and r: \<open>P(x) \<longrightarrow> S \<Longrightarrow> R\<close>
   shows \<open>R\<close>
   by (assumption | rule exI impI major [THEN mp] r)+
 
 text \<open>Courtesy of Krzysztof Grabczewski.\<close>
 lemma disj_imp_disj: \<open>P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S\<close>
   apply (erule disjE)
   apply (rule disjI1) apply assumption
   apply (rule disjI2) apply assumption
   done
 
 ML \<open>
 structure Project_Rule = Project_Rule
 (
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
 )
 \<close>
 
 ML_file \<open>fologic.ML\<close>
 
 lemma thin_refl: \<open>\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W\<close> .
 
 ML \<open>
 structure Hypsubst = Hypsubst
 (
   val dest_eq = FOLogic.dest_eq
-  val dest_Trueprop = FOLogic.dest_Trueprop
+  val dest_Trueprop = \<^dest_judgment>
   val dest_imp = FOLogic.dest_imp
   val eq_reflection = @{thm eq_reflection}
   val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
   val imp_intr = @{thm impI}
   val rev_mp = @{thm rev_mp}
   val subst = @{thm subst}
   val sym = @{thm sym}
   val thin_refl = @{thm thin_refl}
 );
 open Hypsubst;
 \<close>
 
 ML_file \<open>intprover.ML\<close>
 
 
 subsection \<open>Intuitionistic Reasoning\<close>
 
 setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
 
 lemma impE':
   assumes 1: \<open>P \<longrightarrow> Q\<close>
     and 2: \<open>Q \<Longrightarrow> R\<close>
     and 3: \<open>P \<longrightarrow> Q \<Longrightarrow> P\<close>
   shows \<open>R\<close>
 proof -
   from 3 and 1 have \<open>P\<close> .
   with 1 have \<open>Q\<close> by (rule impE)
   with 2 show \<open>R\<close> .
 qed
 
 lemma allE':
   assumes 1: \<open>\<forall>x. P(x)\<close>
     and 2: \<open>P(x) \<Longrightarrow> \<forall>x. P(x) \<Longrightarrow> Q\<close>
   shows \<open>Q\<close>
 proof -
   from 1 have \<open>P(x)\<close> by (rule spec)
   from this and 1 show \<open>Q\<close> by (rule 2)
 qed
 
 lemma notE':
   assumes 1: \<open>\<not> P\<close>
     and 2: \<open>\<not> P \<Longrightarrow> P\<close>
   shows \<open>R\<close>
 proof -
   from 2 and 1 have \<open>P\<close> .
   with 1 show \<open>R\<close> by (rule notE)
 qed
 
 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
 setup \<open>
   Context_Rules.addSWrapper
     (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)
 \<close>
 
 
 lemma iff_not_sym: \<open>\<not> (Q \<longleftrightarrow> P) \<Longrightarrow> \<not> (P \<longleftrightarrow> Q)\<close>
   by iprover
 
 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
 
 lemma eq_commute: \<open>a = b \<longleftrightarrow> b = a\<close>
   by iprover
 
 
 subsection \<open>Polymorphic congruence rules\<close>
 
 lemma subst_context: \<open>a = b \<Longrightarrow> t(a) = t(b)\<close>
   by iprover
 
 lemma subst_context2: \<open>\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)\<close>
   by iprover
 
 lemma subst_context3: \<open>\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)\<close>
   by iprover
 
 text \<open>
   Useful with \<^ML>\<open>eresolve_tac\<close> for proving equalities from known
   equalities.
 
         a = b
         |   |
         c = d
 \<close>
 lemma box_equals: \<open>\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d\<close>
   by iprover
 
 text \<open>Dual of \<open>box_equals\<close>: for proving equalities backwards.\<close>
 lemma simp_equals: \<open>\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b\<close>
   by iprover
 
 
 subsubsection \<open>Congruence rules for predicate letters\<close>
 
 lemma pred1_cong: \<open>a = a' \<Longrightarrow> P(a) \<longleftrightarrow> P(a')\<close>
   by iprover
 
 lemma pred2_cong: \<open>\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> P(a,b) \<longleftrightarrow> P(a',b')\<close>
   by iprover
 
 lemma pred3_cong: \<open>\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> P(a,b,c) \<longleftrightarrow> P(a',b',c')\<close>
   by iprover
 
 text \<open>Special case for the equality predicate!\<close>
 lemma eq_cong: \<open>\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> a = b \<longleftrightarrow> a' = b'\<close>
   by iprover
 
 
 subsection \<open>Atomizing meta-level rules\<close>
 
 lemma atomize_all [atomize]: \<open>(\<And>x. P(x)) \<equiv> Trueprop (\<forall>x. P(x))\<close>
 proof
   assume \<open>\<And>x. P(x)\<close>
   then show \<open>\<forall>x. P(x)\<close> ..
 next
   assume \<open>\<forall>x. P(x)\<close>
   then show \<open>\<And>x. P(x)\<close> ..
 qed
 
 lemma atomize_imp [atomize]: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)\<close>
 proof
   assume \<open>A \<Longrightarrow> B\<close>
   then show \<open>A \<longrightarrow> B\<close> ..
 next
   assume \<open>A \<longrightarrow> B\<close> and \<open>A\<close>
   then show \<open>B\<close> by (rule mp)
 qed
 
 lemma atomize_eq [atomize]: \<open>(x \<equiv> y) \<equiv> Trueprop (x = y)\<close>
 proof
   assume \<open>x \<equiv> y\<close>
   show \<open>x = y\<close> unfolding \<open>x \<equiv> y\<close> by (rule refl)
 next
   assume \<open>x = y\<close>
   then show \<open>x \<equiv> y\<close> by (rule eq_reflection)
 qed
 
 lemma atomize_iff [atomize]: \<open>(A \<equiv> B) \<equiv> Trueprop (A \<longleftrightarrow> B)\<close>
 proof
   assume \<open>A \<equiv> B\<close>
   show \<open>A \<longleftrightarrow> B\<close> unfolding \<open>A \<equiv> B\<close> by (rule iff_refl)
 next
   assume \<open>A \<longleftrightarrow> B\<close>
   then show \<open>A \<equiv> B\<close> by (rule iff_reflection)
 qed
 
 lemma atomize_conj [atomize]: \<open>(A &&& B) \<equiv> Trueprop (A \<and> B)\<close>
 proof
   assume conj: \<open>A &&& B\<close>
   show \<open>A \<and> B\<close>
   proof (rule conjI)
     from conj show \<open>A\<close> by (rule conjunctionD1)
     from conj show \<open>B\<close> by (rule conjunctionD2)
   qed
 next
   assume conj: \<open>A \<and> B\<close>
   show \<open>A &&& B\<close>
   proof -
     from conj show \<open>A\<close> ..
     from conj show \<open>B\<close> ..
   qed
 qed
 
 lemmas [symmetric, rulify] = atomize_all atomize_imp
   and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
 
 
 subsection \<open>Atomizing elimination rules\<close>
 
 lemma atomize_exL[atomize_elim]: \<open>(\<And>x. P(x) \<Longrightarrow> Q) \<equiv> ((\<exists>x. P(x)) \<Longrightarrow> Q)\<close>
   by rule iprover+
 
 lemma atomize_conjL[atomize_elim]: \<open>(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)\<close>
   by rule iprover+
 
 lemma atomize_disjL[atomize_elim]: \<open>((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)\<close>
   by rule iprover+
 
 lemma atomize_elimL[atomize_elim]: \<open>(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop(A)\<close> ..
 
 
 subsection \<open>Calculational rules\<close>
 
 lemma forw_subst: \<open>a = b \<Longrightarrow> P(b) \<Longrightarrow> P(a)\<close>
   by (rule ssubst)
 
 lemma back_subst: \<open>P(a) \<Longrightarrow> a = b \<Longrightarrow> P(b)\<close>
   by (rule subst)
 
 text \<open>
   Note that this list of rules is in reverse order of priorities.
 \<close>
 
 lemmas basic_trans_rules [trans] =
   forw_subst
   back_subst
   rev_mp
   mp
   trans
 
 
 subsection \<open>``Let'' declarations\<close>
 
 nonterminal letbinds and letbind
 
 definition Let :: \<open>['a::{}, 'a => 'b] \<Rightarrow> ('b::{})\<close>
   where \<open>Let(s, f) \<equiv> f(s)\<close>
 
 syntax
   "_bind"       :: \<open>[pttrn, 'a] => letbind\<close>           (\<open>(2_ =/ _)\<close> 10)
   ""            :: \<open>letbind => letbinds\<close>              (\<open>_\<close>)
   "_binds"      :: \<open>[letbind, letbinds] => letbinds\<close>  (\<open>_;/ _\<close>)
   "_Let"        :: \<open>[letbinds, 'a] => 'a\<close>             (\<open>(let (_)/ in (_))\<close> 10)
 
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   "let x = a in e"          == "CONST Let(a, \<lambda>x. e)"
 
 lemma LetI:
   assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close>
   shows \<open>P(let x = t in u(x))\<close>
   unfolding Let_def
   apply (rule refl [THEN assms])
   done
 
 
 subsection \<open>Intuitionistic simplification rules\<close>
 
 lemma conj_simps:
   \<open>P \<and> True \<longleftrightarrow> P\<close>
   \<open>True \<and> P \<longleftrightarrow> P\<close>
   \<open>P \<and> False \<longleftrightarrow> False\<close>
   \<open>False \<and> P \<longleftrightarrow> False\<close>
   \<open>P \<and> P \<longleftrightarrow> P\<close>
   \<open>P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q\<close>
   \<open>P \<and> \<not> P \<longleftrightarrow> False\<close>
   \<open>\<not> P \<and> P \<longleftrightarrow> False\<close>
   \<open>(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)\<close>
   by iprover+
 
 lemma disj_simps:
   \<open>P \<or> True \<longleftrightarrow> True\<close>
   \<open>True \<or> P \<longleftrightarrow> True\<close>
   \<open>P \<or> False \<longleftrightarrow> P\<close>
   \<open>False \<or> P \<longleftrightarrow> P\<close>
   \<open>P \<or> P \<longleftrightarrow> P\<close>
   \<open>P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q\<close>
   \<open>(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)\<close>
   by iprover+
 
 lemma not_simps:
   \<open>\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q\<close>
   \<open>\<not> False \<longleftrightarrow> True\<close>
   \<open>\<not> True \<longleftrightarrow> False\<close>
   by iprover+
 
 lemma imp_simps:
   \<open>(P \<longrightarrow> False) \<longleftrightarrow> \<not> P\<close>
   \<open>(P \<longrightarrow> True) \<longleftrightarrow> True\<close>
   \<open>(False \<longrightarrow> P) \<longleftrightarrow> True\<close>
   \<open>(True \<longrightarrow> P) \<longleftrightarrow> P\<close>
   \<open>(P \<longrightarrow> P) \<longleftrightarrow> True\<close>
   \<open>(P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P\<close>
   by iprover+
 
 lemma iff_simps:
   \<open>(True \<longleftrightarrow> P) \<longleftrightarrow> P\<close>
   \<open>(P \<longleftrightarrow> True) \<longleftrightarrow> P\<close>
   \<open>(P \<longleftrightarrow> P) \<longleftrightarrow> True\<close>
   \<open>(False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P\<close>
   \<open>(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P\<close>
   by iprover+
 
 text \<open>The \<open>x = t\<close> versions are needed for the simplification
   procedures.\<close>
 lemma quant_simps:
   \<open>\<And>P. (\<forall>x. P) \<longleftrightarrow> P\<close>
   \<open>(\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)\<close>
   \<open>(\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)\<close>
   \<open>\<And>P. (\<exists>x. P) \<longleftrightarrow> P\<close>
   \<open>\<exists>x. x = t\<close>
   \<open>\<exists>x. t = x\<close>
   \<open>(\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)\<close>
   \<open>(\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)\<close>
   by iprover+
 
 text \<open>These are NOT supplied by default!\<close>
 lemma distrib_simps:
   \<open>P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R\<close>
   \<open>(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P\<close>
   \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close>
   by iprover+
 
 lemma subst_all:
   \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
   \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
 proof -
   show \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
   proof (rule equal_intr_rule)
     assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close>
     show \<open>PROP P(a)\<close>
       by (rule *) (rule refl)
   next
     fix x
     assume \<open>PROP P(a)\<close> and \<open>x = a\<close>
     from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
       by (rule eq_reflection)
     with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
       by simp
   qed
   show \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
   proof (rule equal_intr_rule)
     assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close>
     show \<open>PROP P(a)\<close>
       by (rule *) (rule refl)
   next
     fix x
     assume \<open>PROP P(a)\<close> and \<open>a = x\<close>
     from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
       by (rule eq_reflection)
     with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
       by simp
   qed
 qed
 
 
 subsubsection \<open>Conversion into rewrite rules\<close>
 
 lemma P_iff_F: \<open>\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)\<close>
   by iprover
 lemma iff_reflection_F: \<open>\<not> P \<Longrightarrow> (P \<equiv> False)\<close>
   by (rule P_iff_F [THEN iff_reflection])
 
 lemma P_iff_T: \<open>P \<Longrightarrow> (P \<longleftrightarrow> True)\<close>
   by iprover
 lemma iff_reflection_T: \<open>P \<Longrightarrow> (P \<equiv> True)\<close>
   by (rule P_iff_T [THEN iff_reflection])
 
 
 subsubsection \<open>More rewrite rules\<close>
 
 lemma conj_commute: \<open>P \<and> Q \<longleftrightarrow> Q \<and> P\<close> by iprover
 lemma conj_left_commute: \<open>P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)\<close> by iprover
 lemmas conj_comms = conj_commute conj_left_commute
 
 lemma disj_commute: \<open>P \<or> Q \<longleftrightarrow> Q \<or> P\<close> by iprover
 lemma disj_left_commute: \<open>P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)\<close> by iprover
 lemmas disj_comms = disj_commute disj_left_commute
 
 lemma conj_disj_distribL: \<open>P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)\<close> by iprover
 lemma conj_disj_distribR: \<open>(P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)\<close> by iprover
 
 lemma disj_conj_distribL: \<open>P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)\<close> by iprover
 lemma disj_conj_distribR: \<open>(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)\<close> by iprover
 
 lemma imp_conj_distrib: \<open>(P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)\<close> by iprover
 lemma imp_conj: \<open>((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))\<close> by iprover
 lemma imp_disj: \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close> by iprover
 
 lemma de_Morgan_disj: \<open>(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)\<close> by iprover
 
 lemma not_ex: \<open>(\<not> (\<exists>x. P(x))) \<longleftrightarrow> (\<forall>x. \<not> P(x))\<close> by iprover
 lemma imp_ex: \<open>((\<exists>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> Q)\<close> by iprover
 
 lemma ex_disj_distrib: \<open>(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> ((\<exists>x. P(x)) \<or> (\<exists>x. Q(x)))\<close>
   by iprover
 
 lemma all_conj_distrib: \<open>(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))\<close>
   by iprover
 
 end
diff --git a/src/FOL/fologic.ML b/src/FOL/fologic.ML
--- a/src/FOL/fologic.ML
+++ b/src/FOL/fologic.ML
@@ -1,52 +1,46 @@
 (*  Title:      FOL/fologic.ML
     Author:     Lawrence C Paulson
 
 Abstract syntax operations for FOL.
 *)
 
 signature FOLOGIC =
 sig
-  val mk_Trueprop: term -> term
-  val dest_Trueprop: term -> term
   val mk_conj: term * term -> term
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
   val dest_imp: term -> term * term
   val dest_conj: term -> term list
   val mk_iff: term * term -> term
   val dest_iff: term -> term * term
   val mk_all: string * typ -> term -> term
   val mk_exists: string * typ -> term -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
 end;
 
 structure FOLogic: FOLOGIC =
 struct
 
-fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
-
-val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
-
 fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
 and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
 and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
 and mk_iff (t1, t2) = \<^Const>\<open>iff for t1 t2\<close>;
 
 val dest_imp = \<^Const_fn>\<open>imp for A B => \<open>(A, B)\<close>\<close>;
 
 fun dest_conj \<^Const_>\<open>conj for t t'\<close> = t :: dest_conj t'
   | dest_conj t = [t];
 
 val dest_iff = \<^Const_fn>\<open>iff for A B => \<open>(A, B)\<close>\<close>;
 
 fun mk_eq (t, u) =
   let val T = fastype_of t
   in \<^Const>\<open>eq T for t u\<close> end;
 
 val dest_eq = \<^Const_fn>\<open>eq _ for lhs rhs => \<open>(lhs, rhs)\<close>\<close>;
 
 fun mk_all (x, T) P = \<^Const>\<open>All T for \<open>absfree (x, T) P\<close>\<close>;
 fun mk_exists (x, T) P = \<^Const>\<open>Ex T for \<open>absfree (x, T) P\<close>\<close>;
 
 end;
diff --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", \<^Type>\<open>i\<close>, free)
           | call_f (free,args) =
                 CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
                             \<^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", \<^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 _ => \<^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", \<^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
+    \<^make_judgment>
       (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
+          \<^make_judgment>
            (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 \<^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/ind_cases.ML b/src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML
+++ b/src/ZF/Tools/ind_cases.ML
@@ -1,72 +1,72 @@
 (*  Title:      ZF/Tools/ind_cases.ML
     Author:     Markus Wenzel, LMU Muenchen
 
 Generic inductive cases facility for (co)inductive definitions.
 *)
 
 signature IND_CASES =
 sig
   val declare: string -> (Proof.context -> conv) -> theory -> theory
   val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
 end;
 
 structure IndCases: IND_CASES =
 struct
 
 
 (* theory data *)
 
 structure IndCasesData = Theory_Data
 (
   type T = (Proof.context -> conv) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
 );
 
 
 fun declare name f = IndCasesData.map (Symtab.update (name, f));
 
 fun smart_cases ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
     val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
-    val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
+    val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (\<^dest_judgment>
       (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
   in
     (case Symtab.lookup (IndCasesData.get thy) c of
       NONE => error ("Unknown inductive cases rule for set " ^ quote c)
     | SOME f => f ctxt (Thm.cterm_of ctxt A))
   end;
 
 
 (* inductive_cases command *)
 
 fun inductive_cases args thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute_cmd ctxt) srcs),
         map (Thm.no_attributes o single o smart_cases ctxt) props));
   in thy |> Global_Theory.note_thmss "" facts |> snd end;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>inductive_cases\<close>
     "create simplified instances of elimination rules (improper)"
     (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
       >> (Toplevel.theory o inductive_cases));
 
 
 (* ind_cases method *)
 
 val _ =
   Theory.setup
     (Method.setup \<^binding>\<open>ind_cases\<close>
       (Scan.lift (Scan.repeat1 Args.embedded_inner_syntax) >>
         (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
       "dynamic case analysis on sets");
 
 end;
 
diff --git a/src/ZF/Tools/induct_tacs.ML b/src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML
+++ b/src/ZF/Tools/induct_tacs.ML
@@ -1,204 +1,204 @@
 (*  Title:      ZF/Tools/induct_tacs.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Induction and exhaustion tactics for Isabelle/ZF.  The theory
 information needed to support them (and to support primrec).  Also a
 function to install other sets as if they were datatypes.
 *)
 
 signature DATATYPE_TACTICS =
 sig
   val exhaust_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
     int -> tactic
   val induct_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
     int -> tactic
   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
   val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
     (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
 end;
 
 
 (** Datatype information, e.g. associated theorems **)
 
 type datatype_info =
   {inductive: bool,             (*true if inductive, not coinductive*)
    constructors : term list,    (*the constructors, as Consts*)
    rec_rewrites : thm list,     (*recursor equations*)
    case_rewrites : thm list,    (*case equations*)
    induct : thm,
    mutual_induct : thm,
    exhaustion : thm};
 
 structure DatatypesData = Theory_Data
 (
   type T = datatype_info Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data : T = Symtab.merge (K true) data;
 );
 
 
 
 (** Constructor information: needed to map constructors to datatypes **)
 
 type constructor_info =
   {big_rec_name : string,     (*name of the mutually recursive set*)
    constructors : term list,  (*the constructors, as Consts*)
    free_iffs    : thm list,   (*freeness simprules*)
    rec_rewrites : thm list};  (*recursor equations*)
 
 
 structure ConstructorsData = Theory_Data
 (
   type T = constructor_info Symtab.table
   val empty = Symtab.empty
   val extend = I
   fun merge data = Symtab.merge (K true) data;
 );
 
 structure DatatypeTactics : DATATYPE_TACTICS =
 struct
 
 fun datatype_info thy name =
   (case Symtab.lookup (DatatypesData.get thy) name of
     SOME info => info
   | NONE => error ("Unknown datatype " ^ quote name));
 
 
 (*Given a variable, find the inductive set associated it in the assumptions*)
 exception Find_tname of string
 
 fun find_tname ctxt var As =
   let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
         | mk_pair _ = raise Match
-      val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
+      val pairs = map_filter (try (mk_pair o \<^dest_judgment>)) As
       val x =
         (case try (dest_Free o Syntax.read_term ctxt) var of
           SOME (x, _) => x
         | _ => raise Find_tname ("Bad variable " ^ quote var))
   in case AList.lookup (op =) pairs x of
        NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
      | SOME t => t
   end;
 
 (** generic exhaustion and induction tactic for datatypes
     Differences from HOL:
       (1) no checking if the induction var occurs in premises, since it always
           appears in one of them, and it's hard to check for other occurrences
       (2) exhaustion works for VARIABLES in the premises, not general terms
 **)
 
 fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ =>
   let
     val thy = Proof_Context.theory_of ctxt
     val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state
     val tn = find_tname ctxt' var (map Thm.term_of asms)
     val rule =
       datatype_info thy tn
       |> (if exh then #exhaustion else #induct)
       |> Thm.transfer thy;
     val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
         (case Thm.prems_of rule of
              [] => error "induction is not available for this datatype"
-           | major::_ => FOLogic.dest_Trueprop major)
+           | major::_ => \<^dest_judgment> major)
   in
     Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
   end
   handle Find_tname msg =>
             if exh then (*try boolean case analysis instead*)
                 case_tac ctxt var fixes i
             else error msg) i state;
 
 val exhaust_tac = exhaust_induct_tac true;
 val induct_tac = exhaust_induct_tac false;
 
 
 (**** declare non-datatype as datatype ****)
 
 fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
   let
     (*analyze the LHS of a case equation to get a constructor*)
     fun const_of \<^Const_>\<open>IFOL.eq _ for \<open>_ $ c\<close> _\<close> = c
       | const_of eqn = error ("Ill-formed case equation: " ^
                               Syntax.string_of_term_global thy eqn);
 
     val constructors =
-        map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
+        map (head_of o const_of o \<^dest_judgment> o Thm.prop_of) case_eqns;
 
-    val \<^Const_>\<open>mem for _ data\<close> = FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
+    val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.prems_of elim));
 
     val Const(big_rec_name, _) = head_of data;
 
     val simps = case_eqns @ recursor_eqns;
 
     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 @{thm TrueI},  (*No need for mutual induction*)
            exhaustion = Thm.trim_context elim};
 
     val con_info =
           {big_rec_name = big_rec_name,
            constructors = constructors,
               (*let primrec handle definition by cases*)
            free_iffs = [],  (*thus we expect the necessary freeness rewrites
                               to be in the simpset already, as is the case for
                               Nat and disjoint sum*)
            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
     thy
     |> Sign.add_path (Long_Name.base_name big_rec_name)
     |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
     |> Sign.parent_path
   end;
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]);
     val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]);
     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
     val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
   in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
 
 
 (* theory setup *)
 
 val _ =
   Theory.setup
     (Method.setup \<^binding>\<open>induct_tac\<close>
       (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
         (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
       "induct_tac emulation (dynamic instantiation!)" #>
     Method.setup \<^binding>\<open>case_tac\<close>
      (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
         (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
       "datatype case_tac emulation (dynamic instantiation!)");
 
 
 (* outer syntax *)
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>rep_datatype\<close> "represent existing set inductively"
     ((\<^keyword>\<open>elimination\<close> |-- Parse.!!! Parse.thm) --
      (\<^keyword>\<open>induction\<close> |-- Parse.!!! Parse.thm) --
      (\<^keyword>\<open>case_eqns\<close> |-- Parse.!!! Parse.thms1) --
      Scan.optional (\<^keyword>\<open>recursor_eqns\<close> |-- Parse.!!! Parse.thms1) []
      >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
 
 end;
 
 val exhaust_tac = DatatypeTactics.exhaust_tac;
 val induct_tac  = DatatypeTactics.induct_tac;
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', \<^Type>\<open>i\<close>), #1 (Ind_Syntax.rule_concl intr))
     in
       fold_rev (FOLogic.mk_exists o Term.dest_Free) exfrees
         (Balanced_Tree.make FOLogic.mk_conj (zeq::prems))
     end;
 
   (*The Part(A,h) terms -- compose injections to make h*)
   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', \<^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', \<^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))
+    Goal.prove_global thy1 [] [] (\<^make_judgment> (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
+               SOME pred => prem :: \<^make_judgment> (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)
+           val concl = \<^make_judgment> (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, \<^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)))
+         (\<^make_judgment> (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 ---> \<^Type>\<open>o\<close>)
            val qconcl =
              fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
                \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
        in  (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
             qconcl)
        end;
 
      val (preds,qconcls) = split_list (map mk_predpair rec_tms);
 
      (*Used to form simultaneous induction lemma*)
      fun mk_rec_imp (rec_tm,pred) =
          \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>;
 
      (*To instantiate the main induction rule*)
      val induct_concl =
-         FOLogic.mk_Trueprop
+         \<^make_judgment>
            (Ind_Syntax.mk_all_imp
             (big_rec_tm,
              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);
+       \<^make_judgment> (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 --> \<^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 \<^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;
+val dest_eqn = FOLogic.dest_eq o \<^dest_judgment>;
 
 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", \<^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),
         \<^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,272 +1,270 @@
 (*  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 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 = \<^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 is_eq_thm th = can FOLogic.dest_eq (\<^dest_judgment> (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)));
+      val goal = Logic.list_implies (map Thm.prop_of prems', \<^make_judgment> (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);
 
 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 = \<^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 = \<^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,118 @@
 (*  Title:      ZF/ind_syntax.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Abstract Syntax functions for Inductive Definitions.
 *)
 
 structure Ind_Syntax =
 struct
 
 (*Print tracing messages during processing of "inductive" theory sections*)
 val trace = Unsynchronized.ref false;
 
 fun traceIt msg thy t =
   if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
   else t;
 
 
 (** Abstract syntax definitions for ZF **)
 
 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
 fun mk_all_imp (A,P) =
   let val T = \<^Type>\<open>i\<close> in
     \<^Const>\<open>All T for
       \<open>Abs ("v", T, \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> A\<close>\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
   end;
 
 fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
 
 (*simple error-checking in the premises of an inductive definition*)
 fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
         error"Premises may not be conjuctive"
   | chk_prem rec_hd \<^Const_>\<open>mem for t X\<close> =
         (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
   | chk_prem rec_hd t =
         (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
 
 (*Return the conclusion of a rule, of the form t:X*)
 fun rule_concl rl =
     let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
     in  (t,X)  end;
 
 (*As above, but return error message if bad*)
 fun rule_concl_msg sign rl = rule_concl rl
     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
                           Syntax.string_of_term_global sign rl);
 
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)
 val equals_CollectD =
     Rule_Insts.read_instantiate \<^context> [((("W", 0), Position.none), "Q")] ["Q"]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
 
 
 (** For datatype definitions **)
 
 (*Constructor name, type, mixfix info;
   internal name from mixfix, datatype sets, full premises*)
 type constructor_spec =
     (string * typ * mixfix) * string * term list * term list;
 
 fun dest_mem \<^Const_>\<open>mem for x A\<close> = (x, A)
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
 (*read a constructor specification*)
 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
     let val prems = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>o\<close>) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> \<^Type>\<open>i\<close>
                 handle TERM _ => error
                     "Bad variable in constructor specification"
     in ((id,T,syn), id, args, prems) end;
 
 val read_constructs = map o map o read_construct;
 
 (*convert constructor specifications into introduction rules*)
 fun mk_intr_tms sg (rec_tm, constructs) =
   let
     fun mk_intr ((id,T,syn), name, args, prems) =
       Logic.list_implies
-        (map FOLogic.mk_Trueprop prems,
-         FOLogic.mk_Trueprop
-            (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
+        (map \<^make_judgment> prems,
+         \<^make_judgment> (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
 
 fun mk_Un (t1, t2) = \<^Const>\<open>Un for t1 t2\<close>;
 
 (*Make a datatype's domain: form the union of its set parameters*)
 fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
       fun is_ind arg = (type_of arg = \<^Type>\<open>i\<close>)
   in  case filter is_ind (args @ cs) of
          [] => \<^Const>\<open>zero\<close>
        | u_args => Balanced_Tree.make mk_Un u_args
   end;
 
 
 (*Includes rules for succ and Pair since they are common constructions*)
 val elim_rls =
   [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
    @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
    make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
 
 
 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   | tryres (th, []) = raise THM("tryres", 0, [th]);
 
 fun gen_make_elim elim_rls rl =
   Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
 
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
 
 end;