diff --git a/src/HOL/Meson.thy b/src/HOL/Meson.thy
--- a/src/HOL/Meson.thy
+++ b/src/HOL/Meson.thy
@@ -1,209 +1,207 @@
 (*  Title:      HOL/Meson.thy
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Tobias Nipkow, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2001  University of Cambridge
 *)
 
 section \<open>MESON Proof Method\<close>
 
 theory Meson
 imports Nat
 begin
 
 subsection \<open>Negation Normal Form\<close>
 
 text \<open>de Morgan laws\<close>
 
 lemma not_conjD: "\<not>(P\<and>Q) \<Longrightarrow> \<not>P \<or> \<not>Q"
   and not_disjD: "\<not>(P\<or>Q) \<Longrightarrow> \<not>P \<and> \<not>Q"
   and not_notD: "\<not>\<not>P \<Longrightarrow> P"
   and not_allD: "\<And>P. \<not>(\<forall>x. P(x)) \<Longrightarrow> \<exists>x. \<not>P(x)"
   and not_exD: "\<And>P. \<not>(\<exists>x. P(x)) \<Longrightarrow> \<forall>x. \<not>P(x)"
   by fast+
 
 text \<open>Removal of \<open>\<longrightarrow>\<close> and \<open>\<longleftrightarrow>\<close> (positive and negative occurrences)\<close>
 
 lemma imp_to_disjD: "P\<longrightarrow>Q \<Longrightarrow> \<not>P \<or> Q"
   and not_impD: "\<not>(P\<longrightarrow>Q) \<Longrightarrow> P \<and> \<not>Q"
   and iff_to_disjD: "P=Q \<Longrightarrow> (\<not>P \<or> Q) \<and> (\<not>Q \<or> P)"
   and not_iffD: "\<not>(P=Q) \<Longrightarrow> (P \<or> Q) \<and> (\<not>P \<or> \<not>Q)"
     \<comment> \<open>Much more efficient than \<^prop>\<open>(P \<and> \<not>Q) \<or> (Q \<and> \<not>P)\<close> for computing CNF\<close>
   and not_refl_disj_D: "x \<noteq> x \<or> P \<Longrightarrow> P"
   by fast+
 
 
 subsection \<open>Pulling out the existential quantifiers\<close>
 
 text \<open>Conjunction\<close>
 
 lemma conj_exD1: "\<And>P Q. (\<exists>x. P(x)) \<and> Q \<Longrightarrow> \<exists>x. P(x) \<and> Q"
   and conj_exD2: "\<And>P Q. P \<and> (\<exists>x. Q(x)) \<Longrightarrow> \<exists>x. P \<and> Q(x)"
   by fast+
 
 
 text \<open>Disjunction\<close>
 
 lemma disj_exD: "\<And>P Q. (\<exists>x. P(x)) \<or> (\<exists>x. Q(x)) \<Longrightarrow> \<exists>x. P(x) \<or> Q(x)"
   \<comment> \<open>DO NOT USE with forall-Skolemization: makes fewer schematic variables!!\<close>
   \<comment> \<open>With ex-Skolemization, makes fewer Skolem constants\<close>
   and disj_exD1: "\<And>P Q. (\<exists>x. P(x)) \<or> Q \<Longrightarrow> \<exists>x. P(x) \<or> Q"
   and disj_exD2: "\<And>P Q. P \<or> (\<exists>x. Q(x)) \<Longrightarrow> \<exists>x. P \<or> Q(x)"
   by fast+
 
 lemma disj_assoc: "(P\<or>Q)\<or>R \<Longrightarrow> P\<or>(Q\<or>R)"
   and disj_comm: "P\<or>Q \<Longrightarrow> Q\<or>P"
   and disj_FalseD1: "False\<or>P \<Longrightarrow> P"
   and disj_FalseD2: "P\<or>False \<Longrightarrow> P"
   by fast+
 
 
 text\<open>Generation of contrapositives\<close>
 
 text\<open>Inserts negated disjunct after removing the negation; P is a literal.
   Model elimination requires assuming the negation of every attempted subgoal,
   hence the negated disjuncts.\<close>
 lemma make_neg_rule: "\<not>P\<or>Q \<Longrightarrow> ((\<not>P\<Longrightarrow>P) \<Longrightarrow> Q)"
 by blast
 
 text\<open>Version for Plaisted's "Postive refinement" of the Meson procedure\<close>
 lemma make_refined_neg_rule: "\<not>P\<or>Q \<Longrightarrow> (P \<Longrightarrow> Q)"
 by blast
 
 text\<open>\<^term>\<open>P\<close> should be a literal\<close>
 lemma make_pos_rule: "P\<or>Q \<Longrightarrow> ((P\<Longrightarrow>\<not>P) \<Longrightarrow> Q)"
 by blast
 
 text\<open>Versions of \<open>make_neg_rule\<close> and \<open>make_pos_rule\<close> that don't
 insert new assumptions, for ordinary resolution.\<close>
 
 lemmas make_neg_rule' = make_refined_neg_rule
 
 lemma make_pos_rule': "\<lbrakk>P\<or>Q; \<not>P\<rbrakk> \<Longrightarrow> Q"
 by blast
 
 text\<open>Generation of a goal clause -- put away the final literal\<close>
 
 lemma make_neg_goal: "\<not>P \<Longrightarrow> ((\<not>P\<Longrightarrow>P) \<Longrightarrow> False)"
 by blast
 
 lemma make_pos_goal: "P \<Longrightarrow> ((P\<Longrightarrow>\<not>P) \<Longrightarrow> False)"
 by blast
 
 
 subsection \<open>Lemmas for Forward Proof\<close>
 
 text\<open>There is a similarity to congruence rules. They are also useful in ordinary proofs.\<close>
 
 (*NOTE: could handle conjunctions (faster?) by
     nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
 lemma conj_forward: "\<lbrakk>P'\<and>Q';  P' \<Longrightarrow> P;  Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P\<and>Q"
 by blast
 
 lemma disj_forward: "\<lbrakk>P'\<or>Q';  P' \<Longrightarrow> P;  Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P\<or>Q"
 by blast
 
 lemma imp_forward: "\<lbrakk>P' \<longrightarrow> Q';  P \<Longrightarrow> P';  Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P \<longrightarrow> Q"
 by blast
 
 lemma imp_forward2: "\<lbrakk>P' \<longrightarrow> Q';  P \<Longrightarrow> P';  P' \<Longrightarrow> Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P \<longrightarrow> Q"
   by blast
 
 (*Version of @{text disj_forward} for removal of duplicate literals*)
 lemma disj_forward2: "\<lbrakk> P'\<or>Q';  P' \<Longrightarrow> P;  \<lbrakk>Q'; P\<Longrightarrow>False\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> P\<or>Q"
 apply blast 
 done
 
 lemma all_forward: "[| \<forall>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<forall>x. P(x)"
 by blast
 
 lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
 by blast
 
 
 subsection \<open>Clausification helper\<close>
 
 lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
 by simp
 
 lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)"
 apply (erule contrapos_np)
 apply clarsimp
 apply (rule cong[where f = F])
 by auto
 
 
 text\<open>Combinator translation helpers\<close>
 
 definition COMBI :: "'a \<Rightarrow> 'a" where
 "COMBI P = P"
 
 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
 "COMBK P Q = P"
 
 definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
 "COMBB P Q R = P (Q R)"
 
 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
 "COMBC P Q R = P R Q"
 
 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
 "COMBS P Q R = P R (Q R)"
 
 lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBS_def) 
 done
 
 lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBI_def) 
 done
 
 lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBK_def) 
 done
 
 lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBB_def) 
 done
 
 lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBC_def) 
 done
 
 
 subsection \<open>Skolemization helpers\<close>
 
 definition skolem :: "'a \<Rightarrow> 'a" where
 "skolem = (\<lambda>x. x)"
 
 lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i::nat))"
 unfolding skolem_def COMBK_def by (rule refl)
 
 lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
-lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
 
 
 subsection \<open>Meson package\<close>
 
 ML_file \<open>Tools/Meson/meson.ML\<close>
 ML_file \<open>Tools/Meson/meson_clausify.ML\<close>
 ML_file \<open>Tools/Meson/meson_tactic.ML\<close>
 
 hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
     not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
     disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
     ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
-    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
-
+    abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I
 end
diff --git a/src/HOL/Tools/Meson/meson_clausify.ML b/src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML
+++ b/src/HOL/Tools/Meson/meson_clausify.ML
@@ -1,385 +1,385 @@
 (*  Title:      HOL/Tools/Meson/meson_clausify.ML
     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     Author:     Jasmin Blanchette, TU Muenchen
 
 Transformation of HOL theorems into CNF forms.
 *)
 
 signature MESON_CLAUSIFY =
 sig
   val new_skolem_var_prefix : string
   val new_nonskolem_var_prefix : string
   val is_zapped_var_name : string -> bool
   val is_quasi_lambda_free : term -> bool
   val introduce_combinators_in_cterm : Proof.context -> cterm -> thm
   val introduce_combinators_in_theorem : Proof.context -> thm -> thm
   val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
   val ss_only : thm list -> Proof.context -> Proof.context
   val cnf_axiom : Meson.simp_options -> Proof.context -> bool -> bool -> int -> thm
     -> (thm * term) option * thm list
 end;
 
 structure Meson_Clausify : MESON_CLAUSIFY =
 struct
 
 (* the extra "Meson" helps prevent clashes (FIXME) *)
 val new_skolem_var_prefix = "MesonSK"
 val new_nonskolem_var_prefix = "MesonV"
 
 fun is_zapped_var_name s =
   exists (fn prefix => String.isPrefix prefix s)
          [new_skolem_var_prefix, new_nonskolem_var_prefix]
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
 val cfalse = Thm.cterm_of \<^theory_context>\<open>HOL\<close> \<^term>\<open>False\<close>;
 val ctp_false = Thm.cterm_of \<^theory_context>\<open>HOL\<close> (HOLogic.mk_Trueprop \<^term>\<open>False\<close>);
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to False. (Cf. "transform_elim_prop" in
    "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   (case Thm.concl_of th of    (*conclusion variable*)
     \<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> =>
       Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th
   | Var (v as (_, \<^Type>\<open>prop\<close>)) =>
       Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th
   | _ => th)
 
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
 fun mk_old_skolem_term_wrapper t =
   let val T = fastype_of t
   in \<^Const>\<open>Meson.skolem T for t\<close> end
 
 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
   | beta_eta_in_abs_body t = Envir.beta_eta_contract t
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun old_skolem_defs th =
   let
     fun dec_sko \<^Const_>\<open>Ex _ for \<open>body as Abs (_, T, p)\<close>\<close> rhss =
         (*Existential: declare a Skolem function, then insert into body and continue*)
         let
           val args = Misc_Legacy.term_frees body
           (* Forms a lambda-abstraction over the formal parameters *)
           val rhs =
             fold_rev (absfree o dest_Free) args
               (HOLogic.choice_const T $ beta_eta_in_abs_body body)
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
       | dec_sko \<^Const_>\<open>All _ for \<open>t as Abs _\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs_global t)) rhss
       | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss
       | dec_sko _ rhss = rhss
   in  dec_sko (Thm.prop_of th) []  end;
 
 
 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
 
 fun is_quasi_lambda_free \<^Const_>\<open>Meson.skolem _ for _\<close> = true
   | is_quasi_lambda_free (t1 $ t2) =
     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   | is_quasi_lambda_free (Abs _) = false
   | is_quasi_lambda_free _ = true
 
 fun abstract ctxt ct =
   let
       val Abs (_, _, body) = Thm.term_of ct
       val (x, cbody) = Thm.dest_abs_global ct
       val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct)
       fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
   in
       case body of
           Const _ => makeK()
         | Free _ => makeK()
         | Var _ => makeK()  (*though Var isn't expected*)
         | Bound 0 => Thm.instantiate' [SOME A] [] @{thm abs_I} (*identity: I*)
         | rator$rand =>
             if Term.is_dependent rator then (*C or S*)
                if Term.is_dependent rand then (*S*)
                  let val crator = Thm.lambda x (Thm.dest_fun cbody)
                      val crand = Thm.lambda x (Thm.dest_arg cbody)
                      val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator))
                      val abs_S' = @{thm abs_S}
                        |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
                      val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
                  in
                    Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
                  end
                else (*C*)
                  let val crator = Thm.lambda x (Thm.dest_fun cbody)
                      val crand = Thm.dest_arg cbody
                      val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator))
                      val abs_C' = @{thm abs_C}
                        |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
                      val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
                  in
                    Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
                  end
             else if Term.is_dependent rand then (*B or eta*)
                if rand = Bound 0 then Thm.eta_conversion ct
                else (*B*)
                  let val crator = Thm.dest_fun cbody
                      val crand = Thm.lambda x (Thm.dest_arg cbody)
                      val (C, B) = Thm.dest_funT (Thm.ctyp_of_cterm crator)
                      val abs_B' = @{thm abs_B}
                       |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
                      val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
                  in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
             else makeK ()
         | _ => raise Fail "abstract: Bad term"
   end;
 
 (* Traverse a theorem, replacing lambda-abstractions with combinators. *)
 fun introduce_combinators_in_cterm ctxt ct =
   if is_quasi_lambda_free (Thm.term_of ct) then
     Thm.reflexive ct
   else case Thm.term_of ct of
     Abs _ =>
     let
       val (cv, cta) = Thm.dest_abs_global ct
       val (v, _) = dest_Free (Thm.term_of cv)
       val u_th = introduce_combinators_in_cterm ctxt cta
       val cu = Thm.rhs_of u_th
       val comb_eq = abstract ctxt (Thm.lambda cv cu)
     in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   | _ $ _ =>
     let val (ct1, ct2) = Thm.dest_comb ct in
         Thm.combination (introduce_combinators_in_cterm ctxt ct1)
                         (introduce_combinators_in_cterm ctxt ct2)
     end
 
 fun introduce_combinators_in_theorem ctxt th =
   if is_quasi_lambda_free (Thm.prop_of th) then
     th
   else
     let
       val th = Drule.eta_contraction_rule th
       val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th)
     in Thm.equal_elim eqth th end
     handle THM (msg, _, _) =>
            (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^
               "\nException message: " ^ msg);
             (* A type variable of sort "{}" will make "abstraction" fail. *)
             TrueI)
 
 (*cterms are used throughout for efficiency*)
 val cTrueprop = Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop;
 
 (*Given an abstraction over n variables, replace the bound variables by free
   ones. Return the body, along with the list of free variables.*)
 fun c_variant_abs_multi (ct0, vars) =
       let val (cv,ct) = Thm.dest_abs_global ct0
       in  c_variant_abs_multi (ct, cv::vars)  end
       handle CTERM _ => (ct0, rev vars);
 
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "\<exists>x. x \<in> A \<and> x \<notin> B \<Longrightarrow> sko A B \<in> A \<and> sko A B \<notin> B" *)
 fun old_skolem_theorem_of_def ctxt rhs0 =
   let
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
     val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
     val T =
       case hilbert of
         Const (_, Type (\<^type_name>\<open>fun\<close>, [_, T])) => T
       | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
     val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
     val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
     val conc =
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.apply cTrueprop
     fun tacf [prem] =
       rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
       THEN resolve_tac ctxt
         [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
           RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1
   in
     Goal.prove_internal ctxt [ex_tm] conc tacf
     |> forall_intr_list frees
     |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
     |> Thm.varifyT_global
   end
 
 fun to_definitional_cnf_with_quantifiers ctxt th =
   let
     val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (Thm.prop_of th))
     val eqth = eqth RS @{thm eq_reflection}
     val eqth = eqth RS @{thm TruepropI}
   in Thm.equal_elim eqth th end
 
 fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
   (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
   "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
   string_of_int index_no ^ "_" ^ Name.desymbolize (SOME false) s
 
 fun cluster_of_zapped_var_name s =
   let val get_int = the o Int.fromString o nth (space_explode "_" s) in
     ((get_int 1, (get_int 2, get_int 3)),
      String.isPrefix new_skolem_var_prefix s)
   end
 
 fun rename_bound_vars_to_be_zapped ax_no =
   let
     fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
       case t of
         (t1 as Const (s, _)) $ Abs (s', T, t') =>
         if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
            s = \<^const_name>\<open>Ex\<close> then
           let
             val skolem = (pos = (s = \<^const_name>\<open>Ex\<close>))
             val (cluster, index_no) =
               if skolem = cluster_skolem then (cluster, index_no)
               else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
             val s' = zapped_var_name cluster index_no s'
           in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end
         else
           t
       | (t1 as Const (s, _)) $ t2 $ t3 =>
         if s = \<^const_name>\<open>Pure.imp\<close> orelse s = \<^const_name>\<open>HOL.implies\<close> then
           t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
         else if s = \<^const_name>\<open>HOL.conj\<close> orelse
                 s = \<^const_name>\<open>HOL.disj\<close> then
           t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3
         else
           t
       | (t1 as Const (s, _)) $ t2 =>
         if s = \<^const_name>\<open>Trueprop\<close> then
           t1 $ aux cluster index_no pos t2
         else if s = \<^const_name>\<open>Not\<close> then
           t1 $ aux cluster index_no (not pos) t2
         else
           t
       | _ => t
   in aux ((ax_no, 0), true) 0 true end
 
 fun zap pos ct =
   ct
   |> (case Thm.term_of ct of
         Const (s, _) $ Abs _ =>
         if s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse
            s = \<^const_name>\<open>Ex\<close> then
           Thm.dest_comb #> snd #> Thm.dest_abs_global #> snd #> zap pos
         else
           Conv.all_conv
       | Const (s, _) $ _ $ _ =>
         if s = \<^const_name>\<open>Pure.imp\<close> orelse s = \<^const_name>\<open>implies\<close> then
           Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
         else if s = \<^const_name>\<open>conj\<close> orelse s = \<^const_name>\<open>disj\<close> then
           Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
         else
           Conv.all_conv
       | Const (s, _) $ _ =>
         if s = \<^const_name>\<open>Trueprop\<close> then Conv.arg_conv (zap pos)
         else if s = \<^const_name>\<open>Not\<close> then Conv.arg_conv (zap (not pos))
         else Conv.all_conv
       | _ => Conv.all_conv)
 
 fun ss_only ths ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths
 
 val cheat_choice =
   \<^prop>\<open>\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)\<close>
   |> Logic.varify_global
   |> Skip_Proof.make_thm \<^theory>
 
 (* Converts an Isabelle theorem into NNF. *)
 fun nnf_axiom simp_options choice_ths new_skolem ax_no th ctxt =
   let
     val thy = Proof_Context.theory_of ctxt
     val th =
       th |> transform_elim_theorem
          |> zero_var_indexes
          |> new_skolem ? Thm.forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
                 |> Meson.cong_extensionalize_thm ctxt
                 |> Meson.abs_extensionalize_thm ctxt
                 |> Meson.make_nnf simp_options ctxt
   in
     if new_skolem then
       let
         fun skolemize choice_ths =
           Meson.skolemize_with_choice_theorems simp_options ctxt choice_ths
           #> simplify (ss_only @{thms all_simps[symmetric]} ctxt)
         val no_choice = null choice_ths
         val pull_out =
           if no_choice then
             simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]} ctxt)
           else
             skolemize choice_ths
         val discharger_th = th |> pull_out
         val discharger_th =
           discharger_th |> Meson.has_too_many_clauses ctxt (Thm.concl_of discharger_th)
                            ? (to_definitional_cnf_with_quantifiers ctxt
                               #> pull_out)
         val zapped_th =
           discharger_th |> Thm.prop_of |> rename_bound_vars_to_be_zapped ax_no
           |> (if no_choice then
                 Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> Thm.cprop_of
               else
                 Thm.cterm_of ctxt)
           |> zap true
         val fixes =
           [] |> Term.add_free_names (Thm.prop_of zapped_th)
              |> filter is_zapped_var_name
         val ctxt' = ctxt |> Variable.add_fixes_direct fixes
         val fully_skolemized_t =
           zapped_th |> singleton (Variable.export ctxt' ctxt)
                     |> Thm.cprop_of |> Thm.dest_equals |> snd |> Thm.term_of
       in
         if exists_subterm (fn Var ((s, _), _) =>
                               String.isPrefix new_skolem_var_prefix s
                             | _ => false) fully_skolemized_t then
           let
             val (fully_skolemized_ct, ctxt) =
               yield_singleton (Variable.import_terms true) fully_skolemized_t ctxt
               |>> Thm.cterm_of ctxt
           in
             (SOME (discharger_th, fully_skolemized_ct),
              (Thm.assume fully_skolemized_ct, ctxt))
           end
        else
          (NONE, (th, ctxt))
       end
     else
       (NONE, (th |> Meson.has_too_many_clauses ctxt (Thm.concl_of th)
                     ? to_definitional_cnf_with_quantifiers ctxt, ctxt))
   end
 
 (* Convert a theorem to CNF, with additional premises due to skolemization. *)
 fun cnf_axiom simp_options ctxt0 new_skolem combinators ax_no th =
   let
     val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0)
     val (opt, (nnf_th, ctxt1)) =
       nnf_axiom simp_options choice_ths new_skolem ax_no th ctxt0
     fun clausify th =
       Meson.make_cnf
        (if new_skolem orelse null choice_ths then []
         else map (old_skolem_theorem_of_def ctxt1) (old_skolem_defs th))
        th ctxt1
     val (cnf_ths, ctxt2) = clausify nnf_th
     fun intr_imp ct th =
-      Thm.instantiate
-        (TVars.empty, Vars.make [(\<^var>\<open>?i::nat\<close>, Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
-        (zero_var_indexes @{thm skolem_COMBK_D})
+      \<^instantiate>\<open>i = \<open>Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no)\<close> in
+        lemma (schematic) \<open>skolem (COMBK P i) \<Longrightarrow> P\<close> for i :: nat
+          by (rule iffD2 [OF skolem_COMBK_iff])\<close>
       RS Thm.implies_intr ct th
   in
     (opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0)
                         ##> (Thm.term_of #> HOLogic.dest_Trueprop
                              #> singleton (Variable.export_terms ctxt2 ctxt0))),
      cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2
                      #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
              |> Variable.export ctxt2 ctxt0
              |> Meson.finish_cnf
              |> map (Thm.close_derivation \<^here>))
   end
   handle THM _ => (NONE, [])
 
 end;
diff --git a/src/HOL/Tools/hologic.ML b/src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML
+++ b/src/HOL/Tools/hologic.ML
@@ -1,721 +1,722 @@
 (*  Title:      HOL/Tools/hologic.ML
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Abstract syntax operations for HOL.
 *)
 
 signature HOLOGIC =
 sig
   val id_const: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
   val mk_obj_eq: thm -> thm
   val Trueprop: term
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
   val Trueprop_conv: conv -> conv
   val mk_induct_forall: typ -> term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
   val Collect_const: typ -> term
   val mk_Collect: string * typ * term -> term
   val mk_mem: term * term -> term
   val dest_mem: term -> term * term
   val mk_set: typ -> term list -> term
   val dest_set: term -> term list
   val mk_UNIV: typ -> term
   val conj_intr: Proof.context -> thm -> thm -> thm
   val conj_elim: Proof.context -> thm -> thm * thm
   val conj_elims: Proof.context -> thm -> thm list
   val conj: term
   val disj: term
   val imp: term
   val Not: term
   val mk_conj: term * term -> term
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
   val mk_not: term -> term
   val dest_conj: term -> term list
   val conjuncts: term -> term list
   val dest_disj: term -> term list
   val disjuncts: term -> term list
   val dest_imp: term -> term * term
   val dest_not: term -> term
   val conj_conv: conv -> conv -> conv
   val eq_const: typ -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
   val eq_conv: conv -> conv -> conv
   val all_const: typ -> term
   val mk_all: string * typ * term -> term
   val list_all: (string * typ) list * term -> term
   val exists_const: typ -> term
   val mk_exists: string * typ * term -> term
   val choice_const: typ -> term
   val class_equal: string
   val mk_binop: string -> term * term -> term
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
   val unitT: typ
   val is_unitT: typ -> bool
   val unit: term
   val is_unit: term -> bool
   val mk_prodT: typ * typ -> typ
   val dest_prodT: typ -> typ * typ
   val pair_const: typ -> typ -> term
   val mk_prod: term * term -> term
   val dest_prod: term -> term * term
   val mk_fst: term -> term
   val mk_snd: term -> term
   val case_prod_const: typ * typ * typ -> term
   val mk_case_prod: term -> term
   val flatten_tupleT: typ -> typ list
   val tupled_lambda: term -> term -> term
   val mk_tupleT: typ list -> typ
   val strip_tupleT: typ -> typ list
   val mk_tuple: term list -> term
   val strip_tuple: term -> term list
   val mk_ptupleT: int list list -> typ list -> typ
   val strip_ptupleT: int list list -> typ -> typ list
   val flat_tupleT_paths: typ -> int list list
   val mk_ptuple: int list list -> typ -> term list -> term
   val strip_ptuple: int list list -> term -> term list
   val flat_tuple_paths: term -> int list list
   val mk_ptupleabs: int list list -> typ -> typ -> term -> term
   val strip_ptupleabs: term -> term * typ list * int list list
   val natT: typ
   val zero: term
   val is_zero: term -> bool
   val mk_Suc: term -> term
   val dest_Suc: term -> term
   val Suc_zero: term
   val mk_nat: int -> term
   val dest_nat: term -> int
   val class_size: string
   val size_const: typ -> term
   val intT: typ
   val one_const: term
   val bit0_const: term
   val bit1_const: term
   val mk_numeral: int -> term
   val dest_numeral: term -> int
   val numeral_const: typ -> term
   val add_numerals: term -> (term * typ) list -> (term * typ) list
   val mk_number: typ -> int -> term
   val dest_number: term -> typ * int
   val code_integerT: typ
   val code_naturalT: typ
   val realT: typ
   val charT: typ
   val mk_char: int -> term
   val dest_char: term -> int
   val listT: typ -> typ
   val nil_const: typ -> term
   val cons_const: typ -> term
   val mk_list: typ -> term list -> term
   val dest_list: term -> term list
   val stringT: typ
   val mk_string: string -> term
   val dest_string: term -> string
   val literalT: typ
   val mk_literal: string -> term
   val dest_literal: term -> string
   val mk_typerep: typ -> term
   val termT: typ
   val term_of_const: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
   val mk_valtermify_app: string -> (string * typ) list -> typ -> term
   val mk_return: typ -> typ -> term -> term
   val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
   val mk_random: typ -> term -> term
 end;
 
 structure HOLogic: HOLOGIC =
 struct
 
 (* functions *)
 
 fun id_const T = Const ("Fun.id", T --> T);
 
 fun mk_comp (f, g) =
   let
     val fT = fastype_of f;
     val gT = fastype_of g;
     val compT = fT --> gT --> domain_type gT --> range_type fT;
   in Const ("Fun.comp", compT) $ f $ g end;
 
 
 (* bool and set *)
 
 val boolN = "HOL.bool";
 val boolT = Type (boolN, []);
 
 fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
 
 fun mk_setT T = Type ("Set.set", [T]);
 
 fun dest_setT (Type ("Set.set", [T])) = T
   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
 
 fun mk_set T ts =
   let
     val sT = mk_setT T;
     val empty = Const ("Orderings.bot_class.bot", sT);
     fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
   in fold_rev insert ts empty end;
 
 fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T);
 
 fun dest_set (Const ("Orderings.bot_class.bot", _)) = []
   | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
   | dest_set t = raise TERM ("dest_set", [t]);
 
 fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T);
 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T) t;
 
 fun mk_mem (x, A) =
   let val setT = fastype_of A in
     Const ("Set.member", dest_setT setT --> setT --> boolT) $ x $ A
   end;
 
 fun dest_mem (Const ("Set.member", _) $ x $ A) = (x, A)
   | dest_mem t = raise TERM ("dest_mem", [t]);
 
 
 (* logic *)
 
 fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
 
 val Trueprop = Const (\<^const_name>\<open>Trueprop\<close>, boolT --> propT);
 
 fun mk_Trueprop P = Trueprop $ P;
 
 fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
 fun Trueprop_conv cv ct =
   (case Thm.term_of ct of
     Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => Conv.arg_conv cv ct
   | _ => raise CTERM ("Trueprop_conv", [ct]))
 
 
 fun conj_intr ctxt thP thQ =
   let
     val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
       handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
-    val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
-  in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
+    val rule = \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q\<close> by (rule conjI)\<close>
+  in Drule.implies_elim_list rule [thP, thQ] end;
 
 fun conj_elim ctxt thPQ =
   let
     val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
       handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
-    val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
-    val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
-    val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
+    val thP =
+      Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> P\<close> by (rule conjunct1)\<close> thPQ;
+    val thQ =
+      Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> Q\<close> by (rule conjunct2)\<close> thPQ;
   in (thP, thQ) end;
 
 fun conj_elims ctxt th =
   let val (th1, th2) = conj_elim ctxt th
   in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th];
 
 val conj = \<^term>\<open>HOL.conj\<close>
 and disj = \<^term>\<open>HOL.disj\<close>
 and imp = \<^term>\<open>implies\<close>
 and Not = \<^term>\<open>Not\<close>;
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
 and mk_imp (t1, t2) = imp $ t1 $ t2
 and mk_not t = Not $ t;
 
 fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
 (*Like dest_conj, but flattens conjunctions however nested*)
 fun conjuncts_aux (Const ("HOL.conj", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
   | conjuncts_aux t conjs = t::conjs;
 
 fun conjuncts t = conjuncts_aux t [];
 
 fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
   | dest_disj t = [t];
 
 (*Like dest_disj, but flattens disjunctions however nested*)
 fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
   | disjuncts_aux t disjs = t::disjs;
 
 fun disjuncts t = disjuncts_aux t [];
 
 fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
 fun dest_not (Const ("HOL.Not", _) $ t) = t
   | dest_not t = raise TERM ("dest_not", [t]);
 
 
 fun conj_conv cv1 cv2 ct =
   (case Thm.term_of ct of
     Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ =>
       Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
   | _ => raise CTERM ("conj_conv", [ct]));
 
 
 fun eq_const T = Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> boolT);
 
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
 
 fun dest_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (lhs, rhs)
   | dest_eq t = raise TERM ("dest_eq", [t])
 
 fun eq_conv cv1 cv2 ct =
   (case Thm.term_of ct of
     Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
   | _ => raise CTERM ("eq_conv", [ct]));
 
 
 fun all_const T = Const ("HOL.All", (T --> boolT) --> boolT);
 fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
 fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
 
 fun exists_const T = Const ("HOL.Ex", (T --> boolT) --> boolT);
 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T) P;
 
 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
 
 val class_equal = "HOL.equal";
 
 
 (* binary operations and relations *)
 
 fun mk_binop c (t, u) =
   let val T = fastype_of t
   in Const (c, T --> T --> T) $ t $ u end;
 
 fun mk_binrel c (t, u) =
   let val T = fastype_of t
   in Const (c, T --> T --> boolT) $ t $ u end;
 
 (*destruct the application of a binary operator. The dummyT case is a crude
   way of handling polymorphic operators.*)
 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
       if c = c' andalso (T=T' orelse T=dummyT) then (t, u)
       else raise TERM ("dest_bin " ^ c, [tm])
   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
 
 
 (* unit *)
 
 val unitT = Type ("Product_Type.unit", []);
 
 fun is_unitT (Type ("Product_Type.unit", [])) = true
   | is_unitT _ = false;
 
 val unit = Const ("Product_Type.Unity", unitT);
 
 fun is_unit (Const ("Product_Type.Unity", _)) = true
   | is_unit _ = false;
 
 
 (* prod *)
 
 fun mk_prodT (T1, T2) = Type ("Product_Type.prod", [T1, T2]);
 
 fun dest_prodT (Type ("Product_Type.prod", [T1, T2])) = (T1, T2)
   | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
 
 fun pair_const T1 T2 = Const ("Product_Type.Pair", T1 --> T2 --> mk_prodT (T1, T2));
 
 fun mk_prod (t1, t2) =
   let val T1 = fastype_of t1 and T2 = fastype_of t2 in
     pair_const T1 T2 $ t1 $ t2
   end;
 
 fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2)
   | dest_prod t = raise TERM ("dest_prod", [t]);
 
 fun mk_fst p =
   let val pT = fastype_of p in
     Const ("Product_Type.prod.fst", pT --> fst (dest_prodT pT)) $ p
   end;
 
 fun mk_snd p =
   let val pT = fastype_of p in
     Const ("Product_Type.prod.snd", pT --> snd (dest_prodT pT)) $ p
   end;
 
 fun case_prod_const (A, B, C) =
   Const ("Product_Type.prod.case_prod", (A --> B --> C) --> mk_prodT (A, B) --> C);
 
 fun mk_case_prod t =
   (case Term.fastype_of t of
     T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
       Const ("Product_Type.prod.case_prod", T --> mk_prodT (A, B) --> C) $ t
   | _ => raise TERM ("mk_case_prod: bad body type", [t]));
 
 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
 fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
   | flatten_tupleT T = [T];
 
 (*abstraction over nested tuples*)
 fun tupled_lambda (x as Free _) b = lambda x b
   | tupled_lambda (x as Var _) b = lambda x b
   | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
       mk_case_prod (tupled_lambda u (tupled_lambda v b))
   | tupled_lambda (Const ("Product_Type.Unity", _)) b =
       Abs ("x", unitT, b)
   | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
 
 
 (* tuples with right-fold structure *)
 
 fun mk_tupleT [] = unitT
   | mk_tupleT Ts = foldr1 mk_prodT Ts;
 
 fun strip_tupleT (Type ("Product_Type.unit", [])) = []
   | strip_tupleT (Type ("Product_Type.prod", [T1, T2])) = T1 :: strip_tupleT T2
   | strip_tupleT T = [T];
 
 fun mk_tuple [] = unit
   | mk_tuple ts = foldr1 mk_prod ts;
 
 fun strip_tuple (Const ("Product_Type.Unity", _)) = []
   | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
   | strip_tuple t = [t];
 
 
 (* tuples with specific arities
 
    an "arity" of a tuple is a list of lists of integers,
    denoting paths to subterms that are pairs
 *)
 
 fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
 
 fun mk_ptupleT ps =
   let
     fun mk p Ts =
       if member (op =) ps p then
         let
           val (T, Ts') = mk (1::p) Ts;
           val (U, Ts'') = mk (2::p) Ts'
         in (mk_prodT (T, U), Ts'') end
       else (hd Ts, tl Ts)
   in fst o mk [] end;
 
 fun strip_ptupleT ps =
   let
     fun factors p T = if member (op =) ps p then (case T of
         Type ("Product_Type.prod", [T1, T2]) =>
           factors (1::p) T1 @ factors (2::p) T2
       | _ => ptuple_err "strip_ptupleT") else [T]
   in factors [] end;
 
 val flat_tupleT_paths =
   let
     fun factors p (Type ("Product_Type.prod", [T1, T2])) =
           p :: factors (1::p) T1 @ factors (2::p) T2
       | factors p _ = []
   in factors [] end;
 
 fun mk_ptuple ps =
   let
     fun mk p T ts =
       if member (op =) ps p then (case T of
           Type ("Product_Type.prod", [T1, T2]) =>
             let
               val (t, ts') = mk (1::p) T1 ts;
               val (u, ts'') = mk (2::p) T2 ts'
             in (pair_const T1 T2 $ t $ u, ts'') end
         | _ => ptuple_err "mk_ptuple")
       else (hd ts, tl ts)
   in fst oo mk [] end;
 
 fun strip_ptuple ps =
   let
     fun dest p t = if member (op =) ps p then (case t of
         Const ("Product_Type.Pair", _) $ t $ u =>
           dest (1::p) t @ dest (2::p) u
       | _ => ptuple_err "strip_ptuple") else [t]
   in dest [] end;
 
 val flat_tuple_paths =
   let
     fun factors p (Const ("Product_Type.Pair", _) $ t $ u) =
           p :: factors (1::p) t @ factors (2::p) u
       | factors p _ = []
   in factors [] end;
 
 (*In mk_ptupleabs ps S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument
   of type S.*)
 fun mk_ptupleabs ps T T3 u =
   let
     fun ap ((p, T) :: pTs) =
           if member (op =) ps p then (case T of
               Type ("Product_Type.prod", [T1, T2]) =>
                 case_prod_const (T1, T2, map snd pTs ---> T3) $
                   ap ((1::p, T1) :: (2::p, T2) :: pTs)
             | _ => ptuple_err "mk_ptupleabs")
           else Abs ("x", T, ap pTs)
       | ap [] =
           let val k = length ps
           in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   in ap [([], T)] end;
 
 val strip_ptupleabs =
   let
     fun strip [] qs Ts t = (t, rev Ts, qs)
       | strip (p :: ps) qs Ts (Const ("Product_Type.prod.case_prod", _) $ t) =
           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
       | strip (p :: ps) qs Ts t = strip ps qs
           (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
           (incr_boundvars 1 t $ Bound 0)
   in strip [[]] [] [] end;
 
 
 (* nat *)
 
 val natT = Type ("Nat.nat", []);
 
 val zero = Const ("Groups.zero_class.zero", natT);
 
 fun is_zero (Const ("Groups.zero_class.zero", _)) = true
   | is_zero _ = false;
 
 fun mk_Suc t = Const ("Nat.Suc", natT --> natT) $ t;
 
 fun dest_Suc (Const ("Nat.Suc", _) $ t) = t
   | dest_Suc t = raise TERM ("dest_Suc", [t]);
 
 val Suc_zero = mk_Suc zero;
 
 fun mk_nat n =
   let
     fun mk 0 = zero
       | mk n = mk_Suc (mk (n - 1));
   in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
 
 fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0
   | dest_nat (Const ("Nat.Suc", _) $ t) = dest_nat t + 1
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 val class_size = "Nat.size";
 
 fun size_const T = Const ("Nat.size_class.size", T --> natT);
 
 
 (* binary numerals and int *)
 
 val numT = Type ("Num.num", []);
 val intT = Type ("Int.int", []);
 
 val one_const = Const ("Num.num.One", numT)
 and bit0_const = Const ("Num.num.Bit0", numT --> numT)
 and bit1_const = Const ("Num.num.Bit1", numT --> numT);
 
 fun mk_numeral i =
   let
     fun mk 1 = one_const
       | mk i =
           let
             val (q, r) = Integer.div_mod i 2
           in (if r = 0 then bit0_const else bit1_const) $ mk q end
   in
     if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
   end
 
 fun dest_numeral (Const ("Num.num.One", _)) = 1
   | dest_numeral (Const ("Num.num.Bit0", _) $ bs) = 2 * dest_numeral bs
   | dest_numeral (Const ("Num.num.Bit1", _) $ bs) = 2 * dest_numeral bs + 1
   | dest_numeral t = raise TERM ("dest_num", [t]);
 
 fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
 
 fun add_numerals (Const ("Num.numeral_class.numeral", Type (_, [_, T])) $ t) = cons (t, T)
   | add_numerals (t $ u) = add_numerals t #> add_numerals u
   | add_numerals (Abs (_, _, t)) = add_numerals t
   | add_numerals _ = I;
 
 fun mk_number T 0 = Const ("Groups.zero_class.zero", T)
   | mk_number T 1 = Const ("Groups.one_class.one", T)
   | mk_number T i =
     if i > 0 then numeral_const T $ mk_numeral i
     else Const ("Groups.uminus_class.uminus", T --> T) $ mk_number T (~ i);
 
 fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
   | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
       (T, dest_numeral t)
   | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", _)) $ t) =
       apsnd (op ~) (dest_number t)
   | dest_number t = raise TERM ("dest_number", [t]);
 
 
 (* code target numerals *)
 
 val code_integerT = Type ("Code_Numeral.integer", []);
 
 val code_naturalT = Type ("Code_Numeral.natural", []);
 
 
 (* real *)
 
 val realT = Type ("Real.real", []);
 
 
 (* list *)
 
 fun listT T = Type ("List.list", [T]);
 
 fun nil_const T = Const ("List.list.Nil", listT T);
 
 fun cons_const T =
   let val lT = listT T
   in Const ("List.list.Cons", T --> lT --> lT) end;
 
 fun mk_list T ts =
   let
     val lT = listT T;
     val Nil = Const ("List.list.Nil", lT);
     fun Cons t u = Const ("List.list.Cons", T --> lT --> lT) $ t $ u;
   in fold_rev Cons ts Nil end;
 
 fun dest_list (Const ("List.list.Nil", _)) = []
   | dest_list (Const ("List.list.Cons", _) $ t $ u) = t :: dest_list u
   | dest_list t = raise TERM ("dest_list", [t]);
 
 
 (* booleans as bits *)
 
 fun mk_bit b = if b = 0 then \<^term>\<open>False\<close>
   else if b = 1 then \<^term>\<open>True\<close>
   else raise TERM ("mk_bit", []);
 
 fun mk_bits len = map mk_bit o Integer.radicify 2 len;
 
 fun dest_bit \<^term>\<open>False\<close> = 0
   | dest_bit \<^term>\<open>True\<close> = 1
   | dest_bit _ = raise TERM ("dest_bit", []);
 
 val dest_bits = Integer.eval_radix 2 o map dest_bit;
 
 
 (* char *)
 
 val charT = Type ("String.char", []);
 
 val Char_const = Const ("String.char.Char", replicate 8 boolT ---> charT);
 
 fun mk_char i =
   if 0 <= i andalso i <= 255
   then list_comb (Char_const, mk_bits 8 i)
   else raise TERM ("mk_char", [])
 
 fun dest_char (Const ("String.char.Char", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ b7) =
       dest_bits [b0, b1, b2, b3, b4, b5, b6, b7]
   | dest_char t = raise TERM ("dest_char", [t]);
 
 
 (* string *)
 
 val stringT = listT charT;
 
 val mk_string = mk_list charT o map (mk_char o ord) o raw_explode;
 val dest_string = implode o map (chr o dest_char) o dest_list;
 
 
 (* literal *)
 
 val literalT = Type ("String.literal", []);
 
 val Literal_const = Const ("String.Literal", replicate 7 boolT ---> literalT --> literalT);
 
 fun mk_literal s = 
   let
     fun mk [] =
           Const ("Groups.zero_class.zero", literalT)
       | mk (c :: cs) =
           list_comb (Literal_const, mk_bits 7 c) $ mk cs;
     val cs = map ord (raw_explode s);
   in
     if forall (fn c => c < 128) cs
     then mk cs
     else raise TERM ("mk_literal", [])
   end;
 
 val dest_literal =
   let
     fun dest (Const ("Groups.zero_class.zero", Type ("String.literal", []))) = []
       | dest (Const ("String.Literal", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
           chr (dest_bits [b0, b1, b2, b3, b4, b5, b6]) :: dest t
       | dest t = raise TERM ("dest_literal", [t]);
   in implode o dest end;
 
 
 (* typerep and term *)
 
 val typerepT = Type ("Typerep.typerep", []);
 
 fun mk_typerep (Type (tyco, Ts)) = Const ("Typerep.typerep.Typerep",
       literalT --> listT typerepT --> typerepT) $ mk_literal tyco
         $ mk_list typerepT (map mk_typerep Ts)
   | mk_typerep (T as TFree _) = Const ("Typerep.typerep_class.typerep",
       Term.itselfT T --> typerepT) $ Logic.mk_type T;
 
 val termT = Type ("Code_Evaluation.term", []);
 
 fun term_of_const T = Const ("Code_Evaluation.term_of_class.term_of", T --> termT);
 
 fun mk_term_of T t = term_of_const T $ t;
 
 fun reflect_term (Const (c, T)) =
       Const ("Code_Evaluation.Const", literalT --> typerepT --> termT)
         $ mk_literal c $ mk_typerep T
   | reflect_term (t1 $ t2) =
       Const ("Code_Evaluation.App", termT --> termT --> termT)
         $ reflect_term t1 $ reflect_term t2
   | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
   | reflect_term t = t;
 
 fun mk_valtermify_app c vs T =
   let
     fun termifyT T = mk_prodT (T, unitT --> termT);
     fun valapp T T' = Const ("Code_Evaluation.valapp",
       termifyT (T --> T') --> termifyT T --> termifyT T');
     fun mk_fTs [] _ = []
       | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
     val Ts = map snd vs;
     val t = Const (c, Ts ---> T);
     val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
     fun app (fT, (v, T)) t = valapp T fT $ t $ Free (v, termifyT T);
   in fold app (mk_fTs Ts T ~~ vs) tt end;
 
 
 (* open state monads *)
 
 fun mk_return T U x = pair_const T U $ x;
 
 fun mk_ST clauses t U (someT, V) =
   let
     val R = case someT of SOME T => mk_prodT (T, V) | NONE => V
     fun mk_clause ((t, U), SOME (v, T)) (t', U') =
           (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R)
             $ t $ lambda (Free (v, T)) t', U)
       | mk_clause ((t, U), NONE) (t', U') =
           (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R)
             $ t $ t', U)
   in fold_rev mk_clause clauses (t, U) |> fst end;
 
 
 (* random seeds *)
 
 val random_seedT = mk_prodT (code_naturalT, code_naturalT);
 
 fun mk_random T t = Const ("Quickcheck_Random.random_class.random", code_naturalT
   --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
 
 end;
diff --git a/src/HOL/Tools/record.ML b/src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML
+++ b/src/HOL/Tools/record.ML
@@ -1,2409 +1,2408 @@
 (*  Title:      HOL/Tools/record.ML
     Author:     Wolfgang Naraschewski, TU Muenchen
     Author:     Markus Wenzel, TU Muenchen
     Author:     Norbert Schirmer, TU Muenchen
     Author:     Thomas Sewell, NICTA
 
 Extensible records with structural subtyping.
 *)
 
 signature RECORD =
 sig
   val type_abbr: bool Config.T
   val type_as_fields: bool Config.T
   val timing: bool Config.T
 
   type info =
    {args: (string * sort) list,
     parent: (typ list * string) option,
     fields: (string * typ) list,
     extension: (string * typ list),
     ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
     select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
     fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
     surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
     cases: thm, simps: thm list, iffs: thm list}
   val get_info: theory -> string -> info option
   val the_info: theory -> string -> info
   val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
   val add_record: {overloaded: bool} -> (string * sort) list * binding ->
     (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory
 
   val last_extT: typ -> (string * typ list) option
   val dest_recTs: typ -> (string * typ list) list
   val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
   val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
   val get_parent: theory -> string -> (typ list * string) option
   val get_extension: theory -> string -> (string * typ list) option
   val get_extinjects: theory -> thm list
   val get_simpset: theory -> simpset
   val simproc: simproc
   val eq_simproc: simproc
   val upd_simproc: simproc
   val split_simproc: (term -> int) -> simproc
   val ex_sel_eq_simproc: simproc
   val split_tac: Proof.context -> int -> tactic
   val split_simp_tac: Proof.context -> thm list -> (term -> int) -> int -> tactic
   val split_wrapper: string * (Proof.context -> wrapper)
 
   val pretty_recT: Proof.context -> typ -> Pretty.T
   val string_of_record: Proof.context -> string -> string
 
   val codegen: bool Config.T
   val updateN: string
   val ext_typeN: string
   val extN: string
 end;
 
 
 signature ISO_TUPLE_SUPPORT =
 sig
   val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list ->
     typ * typ -> theory -> (term * term) * theory
   val mk_cons_tuple: term * term -> term
   val dest_cons_tuple: term -> term * term
   val iso_tuple_intros_tac: Proof.context -> int -> tactic
 end;
 
 structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
 struct
 
 val isoN = "_Tuple_Iso";
 
 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
 
 val tuple_iso_tuple = (\<^const_name>\<open>Record.tuple_iso_tuple\<close>, @{thm tuple_iso_tuple});
 
 structure Iso_Tuple_Thms = Theory_Data
 (
   type T = thm Symtab.table;
   val empty = Symtab.make [tuple_iso_tuple];
   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
 
 fun get_typedef_info tyco vs
     (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
   let
     val exists_thm =
       UNIV_I
       |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
     val proj_constr = Abs_inverse OF [exists_thm];
     val absT = Type (tyco, map TFree vs);
   in
     thy
     |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
   end
 
 fun do_typedef overloaded raw_tyco repT raw_vs thy =
   let
     val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
     |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
         (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
           (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
 
 fun mk_cons_tuple (t, u) =
   let val (A, B) = apply2 fastype_of (t, u)
   in \<^Const>\<open>iso_tuple_cons \<^Type>\<open>prod A B\<close> A B for \<^Const>\<open>tuple_iso_tuple A B\<close> t u\<close> end;
 
 fun dest_cons_tuple \<^Const_>\<open>iso_tuple_cons _ _ _ for \<open>Const _\<close> t u\<close> = (t, u)
   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
 
 fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
   let
     val repT = HOLogic.mk_prodT (leftT, rightT);
 
     val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
       thy
       |> do_typedef overloaded b repT alphas
       ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
     val typ_ctxt = Proof_Context.init_global typ_thy;
 
     (*construct a type and body for the isomorphism constant by
       instantiating the theorem to which the definition will be applied*)
     val intro_inst =
       rep_inject RS
         infer_instantiate typ_ctxt
           [(("abst", 0), Thm.cterm_of typ_ctxt absC)] iso_tuple_intro;
     val (_, body) = Logic.dest_equals (List.last (Thm.prems_of intro_inst));
     val isomT = fastype_of body;
     val isom_binding = Binding.suffix_name isoN b;
     val isom_name = Sign.full_name typ_thy isom_binding;
     val isom = Const (isom_name, isomT);
 
     val ([isom_def], cdef_thy) =
       typ_thy
       |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
       |> Global_Theory.add_defs false
         [((Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
 
     val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
     val cons = \<^Const>\<open>iso_tuple_cons absT leftT rightT\<close>;
 
     val thm_thy =
       cdef_thy
       |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
       |> Sign.restore_naming thy
   in
     ((isom, cons $ isom), thm_thy)
   end;
 
 fun iso_tuple_intros_tac ctxt =
   resolve_from_net_tac ctxt iso_tuple_intros THEN'
   CSUBGOAL (fn (cgoal, i) =>
     let
       val goal = Thm.term_of cgoal;
 
       val isthms = Iso_Tuple_Thms.get (Proof_Context.theory_of ctxt);
       fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
 
       val goal' = Envir.beta_eta_contract goal;
       val is =
         (case goal' of
           \<^Const_>\<open>Trueprop for \<^Const>\<open>isomorphic_tuple _ _ _ for \<open>Const is\<close>\<close>\<close> => is
         | _ => err "unexpected goal format" goal');
       val isthm =
         (case Symtab.lookup isthms (#1 is) of
           SOME isthm => isthm
         | NONE => err "no thm found for constant" (Const is));
     in resolve_tac ctxt [isthm] i end);
 
 end;
 
 
 structure Record: RECORD =
 struct
 
 val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
 val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};
 
 val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
 val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
 val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
 val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};
 
 val updacc_foldE = @{thm update_accessor_congruence_foldE};
 val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
 val updacc_noopE = @{thm update_accessor_noopE};
 val updacc_noop_compE = @{thm update_accessor_noop_compE};
 val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
 
 val codegen = Attrib.setup_config_bool \<^binding>\<open>record_codegen\<close> (K true);
 
 
 (** name components **)
 
 val rN = "r";
 val wN = "w";
 val moreN = "more";
 val schemeN = "_scheme";
 val ext_typeN = "_ext";
 val inner_typeN = "_inner";
 val extN ="_ext";
 val updateN = "_update";
 val makeN = "make";
 val fields_selN = "fields";
 val extendN = "extend";
 val truncateN = "truncate";
 
 
 
 (*** utilities ***)
 
 fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));
 
 
 (* timing *)
 
 val timing = Attrib.setup_config_bool \<^binding>\<open>record_timing\<close> (K false);
 fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
 fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
 
 
 (* syntax *)
 
 val Trueprop = HOLogic.mk_Trueprop;
 
 infix 0 :== ===;
 infixr 0 ==>;
 
 val op :== = Misc_Legacy.mk_defpair;
 val op === = Trueprop o HOLogic.mk_eq;
 val op ==> = Logic.mk_implies;
 
 
 (* constructor *)
 
 fun mk_ext (name, T) ts =
   let val Ts = map fastype_of ts
   in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
 
 
 (* selector *)
 
 fun mk_selC sT (c, T) = (c, sT --> T);
 
 fun mk_sel s (c, T) =
   let val sT = fastype_of s
   in Const (mk_selC sT (c, T)) $ s end;
 
 
 (* updates *)
 
 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
 
 fun mk_upd' sfx c v sT =
   let val vT = domain_type (fastype_of v);
   in Const (mk_updC sfx sT (c, vT)) $ v end;
 
 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
 
 
 (* types *)
 
 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
       (case try (unsuffix ext_typeN) c_ext_type of
         NONE => raise TYPE ("Record.dest_recT", [typ], [])
       | SOME c => ((c, Ts), List.last Ts))
   | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
 
 val is_recT = can dest_recT;
 
 fun dest_recTs T =
   let val ((c, Ts), U) = dest_recT T
   in (c, Ts) :: dest_recTs U
   end handle TYPE _ => [];
 
 fun last_extT T =
   let val ((c, Ts), U) = dest_recT T in
     (case last_extT U of
       NONE => SOME (c, Ts)
     | SOME l => SOME l)
   end handle TYPE _ => NONE;
 
 fun rec_id i T =
   let
     val rTs = dest_recTs T;
     val rTs' = if i < 0 then rTs else take i rTs;
   in implode (map #1 rTs') end;
 
 
 
 (*** extend theory by record definition ***)
 
 (** record info **)
 
 (* type info and parent_info *)
 
 type info =
  {args: (string * sort) list,
   parent: (typ list * string) option,
   fields: (string * typ) list,
   extension: (string * typ list),
 
   ext_induct: thm,
   ext_inject: thm,
   ext_surjective: thm,
   ext_split: thm,
   ext_def: thm,
 
   select_convs: thm list,
   update_convs: thm list,
   select_defs: thm list,
   update_defs: thm list,
   fold_congs: thm list,  (* potentially used in L4.verified *)
   unfold_congs: thm list,  (* potentially used in L4.verified *)
   splits: thm list,
   defs: thm list,
 
   surjective: thm,
   equality: thm,
   induct_scheme: thm,
   induct: thm,
   cases_scheme: thm,
   cases: thm,
 
   simps: thm list,
   iffs: thm list};
 
 fun make_info args parent fields extension
     ext_induct ext_inject ext_surjective ext_split ext_def
     select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
     surjective equality induct_scheme induct cases_scheme cases
     simps iffs : info =
  {args = args, parent = parent, fields = fields, extension = extension,
   ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
   ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
   update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
   fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
   surjective = surjective, equality = equality, induct_scheme = induct_scheme,
   induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
 
 type parent_info =
  {name: string,
   fields: (string * typ) list,
   extension: (string * typ list),
   induct_scheme: thm,
   ext_def: thm};
 
 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
  {name = name, fields = fields, extension = extension,
   ext_def = ext_def, induct_scheme = induct_scheme};
 
 
 (* theory data *)
 
 type data =
  {records: info Symtab.table,
   sel_upd:
    {selectors: (int * bool) Symtab.table,
     updates: string Symtab.table,
     simpset: simpset,
     defset: simpset},
   equalities: thm Symtab.table,
   extinjects: thm list,
   extsplit: thm Symtab.table,  (*maps extension name to split rule*)
   splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
   extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
   fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
 
 fun make_data
     records sel_upd equalities extinjects extsplit splits extfields fieldext =
  {records = records, sel_upd = sel_upd,
   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   extfields = extfields, fieldext = fieldext }: data;
 
 structure Data = Theory_Data
 (
   type T = data;
   val empty =
     make_data Symtab.empty
       {selectors = Symtab.empty, updates = Symtab.empty,
         simpset = HOL_basic_ss, defset = HOL_basic_ss}
        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   fun merge
    ({records = recs1,
      sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
      equalities = equalities1,
      extinjects = extinjects1,
      extsplit = extsplit1,
      splits = splits1,
      extfields = extfields1,
      fieldext = fieldext1},
     {records = recs2,
      sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},
      equalities = equalities2,
      extinjects = extinjects2,
      extsplit = extsplit2,
      splits = splits2,
      extfields = extfields2,
      fieldext = fieldext2}) =
     make_data
       (Symtab.merge (K true) (recs1, recs2))
       {selectors = Symtab.merge (K true) (sels1, sels2),
         updates = Symtab.merge (K true) (upds1, upds2),
         simpset = Simplifier.merge_ss (ss1, ss2),
         defset = Simplifier.merge_ss (ds1, ds2)}
       (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
       (Thm.merge_thms (extinjects1, extinjects2))
       (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
       (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
           Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
           Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
       (Symtab.merge (K true) (extfields1, extfields2))
       (Symtab.merge (K true) (fieldext1, fieldext2));
 );
 
 
 (* access 'records' *)
 
 val get_info = Symtab.lookup o #records o Data.get;
 
 fun the_info thy name =
   (case get_info thy name of
     SOME info => info
   | NONE => error ("Unknown record type " ^ quote name));
 
 fun put_record name info =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     make_data (Symtab.update (name, info) records)
       sel_upd equalities extinjects extsplit splits extfields fieldext);
 
 
 (* access 'sel_upd' *)
 
 val get_sel_upd = #sel_upd o Data.get;
 
 val is_selector = Symtab.defined o #selectors o get_sel_upd;
 val get_updates = Symtab.lookup o #updates o get_sel_upd;
 
 val get_simpset = #simpset o get_sel_upd;
 val get_sel_upd_defs = #defset o get_sel_upd;
 
 fun get_update_details u thy =
   let val sel_upd = get_sel_upd thy in
     (case Symtab.lookup (#updates sel_upd) u of
       SOME s =>
         let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
         in SOME (s, dep, ismore) end
     | NONE => NONE)
   end;
 
 fun put_sel_upd names more depth simps defs thy =
   let
     val ctxt0 = Proof_Context.init_global thy;
 
     val all = names @ [more];
     val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
     val upds = map (suffix updateN) all ~~ all;
 
     val {records, sel_upd = {selectors, updates, simpset, defset},
       equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
     val data =
       make_data records
         {selectors = fold Symtab.update_new sels selectors,
           updates = fold Symtab.update_new upds updates,
           simpset = simpset_map ctxt0 (fn ctxt => ctxt addsimps simps) simpset,
           defset = simpset_map ctxt0 (fn ctxt => ctxt addsimps defs) defset}
          equalities extinjects extsplit splits extfields fieldext;
   in Data.put data thy end;
 
 
 (* access 'equalities' *)
 
 fun add_equalities name thm =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     make_data records sel_upd
       (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
 
 val get_equalities = Symtab.lookup o #equalities o Data.get;
 
 
 (* access 'extinjects' *)
 
 fun add_extinjects thm =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
       extsplit splits extfields fieldext);
 
 val get_extinjects = rev o #extinjects o Data.get;
 
 
 (* access 'extsplit' *)
 
 fun add_extsplit name thm =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     make_data records sel_upd equalities extinjects
       (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
 
 
 (* access 'splits' *)
 
 fun add_splits name thmP =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     make_data records sel_upd equalities extinjects extsplit
       (Symtab.update_new (name, thmP) splits) extfields fieldext);
 
 val get_splits = Symtab.lookup o #splits o Data.get;
 
 
 (* parent/extension of named record *)
 
 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
 
 
 (* access 'extfields' *)
 
 fun add_extfields name fields =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     make_data records sel_upd equalities extinjects extsplit splits
       (Symtab.update_new (name, fields) extfields) fieldext);
 
 val get_extfields = Symtab.lookup o #extfields o Data.get;
 
 fun get_extT_fields thy T =
   let
     val ((name, Ts), moreT) = dest_recT T;
     val recname =
       let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
       in Long_Name.implode (rev (nm :: rst)) end;
     val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
     val {records, extfields, ...} = Data.get thy;
     val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
 
     val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
     val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
   in (fields', (more, moreT)) end;
 
 fun get_recT_fields thy T =
   let
     val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
     val (rest_fields, rest_more) =
       if is_recT root_moreT then get_recT_fields thy root_moreT
       else ([], (root_more, root_moreT));
   in (root_fields @ rest_fields, rest_more) end;
 
 
 (* access 'fieldext' *)
 
 fun add_fieldext extname_types fields =
   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
     let
       val fieldext' =
         fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
     in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
 
 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
 
 
 (* parent records *)
 
 local
 
 fun add_parents _ NONE = I
   | add_parents thy (SOME (types, name)) =
       let
         fun err msg = error (msg ^ " parent record " ^ quote name);
 
         val {args, parent, ...} =
           (case get_info thy name of SOME info => info | NONE => err "Unknown");
         val _ = if length types <> length args then err "Bad number of arguments for" else ();
 
         fun bad_inst ((x, S), T) =
           if Sign.of_sort thy (T, S) then NONE else SOME x
         val bads = map_filter bad_inst (args ~~ types);
         val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
 
         val inst = args ~~ types;
         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
         val parent' = Option.map (apfst (map subst)) parent;
       in cons (name, inst) #> add_parents thy parent' end;
 
 in
 
 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
 
 fun get_parent_info thy parent =
   add_parents thy parent [] |> map (fn (name, inst) =>
     let
       val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
       val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
       val fields' = map (apsnd subst) fields;
       val extension' = apsnd (map subst) extension;
     in make_parent_info name fields' extension' ext_def induct_scheme end);
 
 end;
 
 
 
 (** concrete syntax for records **)
 
 (* parse translations *)
 
 local
 
 fun split_args (field :: fields) ((name, arg) :: fargs) =
       if can (unsuffix name) field then
         let val (args, rest) = split_args fields fargs
         in (arg :: args, rest) end
       else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
   | split_args [] (fargs as (_ :: _)) = ([], fargs)
   | split_args (_ :: _) [] = raise Fail "expecting more fields"
   | split_args _ _ = ([], []);
 
 fun field_type_tr ((Const (\<^syntax_const>\<open>_field_type\<close>, _) $ Const (name, _) $ arg)) =
       (name, arg)
   | field_type_tr t = raise TERM ("field_type_tr", [t]);
 
 fun field_types_tr (Const (\<^syntax_const>\<open>_field_types\<close>, _) $ t $ u) =
       field_type_tr t :: field_types_tr u
   | field_types_tr t = [field_type_tr t];
 
 fun record_field_types_tr more ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
 
     fun mk_ext (fargs as (name, _) :: _) =
           (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
             SOME (ext, alphas) =>
               (case get_extfields thy ext of
                 SOME fields =>
                   let
                     val (fields', _) = split_last fields;
                     val types = map snd fields';
                     val (args, rest) = split_args (map fst fields') fargs
                       handle Fail msg => err msg;
                     val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
                     val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
                     val vartypes = map varifyT types;
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
                       handle Type.TYPE_MATCH => err "type is no proper record (extension)";
                     val alphas' =
                       map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
                         (#1 (split_last alphas));
 
                     val more' = mk_ext rest;
                   in
                     list_comb
                       (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
                   end
               | NONE => err ("no fields defined for " ^ quote ext))
           | NONE => err (quote name ^ " is no proper field"))
       | mk_ext [] = more;
   in
     mk_ext (field_types_tr t)
   end;
 
 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const \<^type_syntax>\<open>unit\<close>) ctxt t
   | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
 
 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
   | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
 
 
 fun field_tr ((Const (\<^syntax_const>\<open>_field\<close>, _) $ Const (name, _) $ arg)) = (name, arg)
   | field_tr t = raise TERM ("field_tr", [t]);
 
 fun fields_tr (Const (\<^syntax_const>\<open>_fields\<close>, _) $ t $ u) = field_tr t :: fields_tr u
   | fields_tr t = [field_tr t];
 
 fun record_fields_tr more ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
 
     fun mk_ext (fargs as (name, _) :: _) =
           (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
             SOME (ext, _) =>
               (case get_extfields thy ext of
                 SOME fields =>
                   let
                     val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
                       handle Fail msg => err msg;
                     val more' = mk_ext rest;
                   in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
               | NONE => err ("no fields defined for " ^ quote ext))
           | NONE => err (quote name ^ " is no proper field"))
       | mk_ext [] = more;
   in mk_ext (fields_tr t) end;
 
 fun record_tr ctxt [t] = record_fields_tr (Syntax.const \<^const_syntax>\<open>Unity\<close>) ctxt t
   | record_tr _ ts = raise TERM ("record_tr", ts);
 
 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
   | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
 
 
 fun field_update_tr (Const (\<^syntax_const>\<open>_field_update\<close>, _) $ Const (name, _) $ arg) =
       Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
   | field_update_tr t = raise TERM ("field_update_tr", [t]);
 
 fun field_updates_tr (Const (\<^syntax_const>\<open>_field_updates\<close>, _) $ t $ u) =
       field_update_tr t :: field_updates_tr u
   | field_updates_tr t = [field_update_tr t];
 
 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
   | record_update_tr ts = raise TERM ("record_update_tr", ts);
 
 in
 
 val _ =
   Theory.setup
    (Sign.parse_translation
      [(\<^syntax_const>\<open>_record_update\<close>, K record_update_tr),
       (\<^syntax_const>\<open>_record\<close>, record_tr),
       (\<^syntax_const>\<open>_record_scheme\<close>, record_scheme_tr),
       (\<^syntax_const>\<open>_record_type\<close>, record_type_tr),
       (\<^syntax_const>\<open>_record_type_scheme\<close>, record_type_scheme_tr)]);
 
 end;
 
 
 (* print translations *)
 
 val type_abbr = Attrib.setup_config_bool \<^binding>\<open>record_type_abbr\<close> (K true);
 val type_as_fields = Attrib.setup_config_bool \<^binding>\<open>record_type_as_fields\<close> (K true);
 
 
 local
 
 (* FIXME early extern (!??) *)
 (* FIXME Syntax.free (??) *)
 fun field_type_tr' (c, t) = Syntax.const \<^syntax_const>\<open>_field_type\<close> $ Syntax.const c $ t;
 
 fun field_types_tr' (t, u) = Syntax.const \<^syntax_const>\<open>_field_types\<close> $ t $ u;
 
 fun record_type_tr' ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val T = Syntax_Phases.decode_typ t;
     val varifyT = varifyT (Term.maxidx_of_typ T + 1);
 
     fun strip_fields T =
       (case T of
         Type (ext, args as _ :: _) =>
           (case try (unsuffix ext_typeN) ext of
             SOME ext' =>
               (case get_extfields thy ext' of
                 SOME (fields as (x, _) :: _) =>
                   (case get_fieldext thy x of
                     SOME (_, alphas) =>
                      (let
                         val (f :: fs, _) = split_last fields;
                         val fields' =
                           apfst (Proof_Context.extern_const ctxt) f ::
                             map (apfst Long_Name.base_name) fs;
                         val (args', more) = split_last args;
                         val alphavars = map varifyT (#1 (split_last alphas));
                         val subst = Type.raw_matches (alphavars, args') Vartab.empty;
                         val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
                       in fields'' @ strip_fields more end
                       handle Type.TYPE_MATCH => [("", T)])
                   | _ => [("", T)])
               | _ => [("", T)])
           | _ => [("", T)])
       | _ => [("", T)]);
 
     val (fields, (_, moreT)) = split_last (strip_fields T);
     val _ = null fields andalso raise Match;
     val u =
       foldr1 field_types_tr'
         (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
   in
     if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
     else if moreT = HOLogic.unitT then Syntax.const \<^syntax_const>\<open>_record_type\<close> $ u
     else
       Syntax.const \<^syntax_const>\<open>_record_type_scheme\<close> $ u $
         Syntax_Phases.term_of_typ ctxt moreT
   end;
 
 (*try to reconstruct the record name type abbreviation from
   the (nested) extension types*)
 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   let
     val T = Syntax_Phases.decode_typ tm;
     val varifyT = varifyT (maxidx_of_typ T + 1);
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)
       in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
 
     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   in
     if Config.get ctxt type_abbr then
       (case last_extT T of
         SOME (name, _) =>
           if name = last_ext then
             let val subst = match schemeT T in
               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
               then mk_type_abbr subst abbr alphas
               else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
             end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
           else raise Match (*give print translation of specialised record a chance*)
       | _ => raise Match)
     else record_type_tr' ctxt tm
   end;
 
 in
 
 fun record_ext_type_tr' name =
   let
     val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
     fun tr' ctxt ts =
       record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
   in (ext_type_name, tr') end;
 
 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
   let
     val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
     fun tr' ctxt ts =
       record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
         (list_comb (Syntax.const ext_type_name, ts));
   in (ext_type_name, tr') end;
 
 end;
 
 
 local
 
 (* FIXME Syntax.free (??) *)
 fun field_tr' (c, t) = Syntax.const \<^syntax_const>\<open>_field\<close> $ Syntax.const c $ t;
 fun fields_tr' (t, u) = Syntax.const \<^syntax_const>\<open>_fields\<close> $ t $ u;
 
 fun record_tr' ctxt t =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun strip_fields t =
       (case strip_comb t of
         (Const (ext, _), args as (_ :: _)) =>
           (case try (Lexicon.unmark_const o unsuffix extN) ext of
             SOME ext' =>
               (case get_extfields thy ext' of
                 SOME fields =>
                  (let
                     val (f :: fs, _) = split_last (map fst fields);
                     val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
                     val (args', more) = split_last args;
                   in (fields' ~~ args') @ strip_fields more end
                   handle ListPair.UnequalLengths => [("", t)])
               | NONE => [("", t)])
           | NONE => [("", t)])
        | _ => [("", t)]);
 
     val (fields, (_, more)) = split_last (strip_fields t);
     val _ = null fields andalso raise Match;
     val u = foldr1 fields_tr' (map field_tr' fields);
   in
     (case more of
       Const (\<^const_syntax>\<open>Unity\<close>, _) => Syntax.const \<^syntax_const>\<open>_record\<close> $ u
     | _ => Syntax.const \<^syntax_const>\<open>_record_scheme\<close> $ u $ more)
   end;
 
 in
 
 fun record_ext_tr' name =
   let
     val ext_name = Lexicon.mark_const (name ^ extN);
     fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
   in (ext_name, tr') end;
 
 end;
 
 
 local
 
 fun dest_update ctxt c =
   (case try Lexicon.unmark_const c of
     SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
   | NONE => NONE);
 
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
       (case dest_update ctxt c of
         SOME name =>
           (case try Syntax_Trans.const_abs_tr' k of
             SOME t =>
               apfst (cons (Syntax.const \<^syntax_const>\<open>_field_update\<close> $ Syntax.free name $ t))
                 (field_updates_tr' ctxt u)
           | NONE => ([], tm))
       | NONE => ([], tm))
   | field_updates_tr' _ tm = ([], tm);
 
 fun record_update_tr' ctxt tm =
   (case field_updates_tr' ctxt tm of
     ([], _) => raise Match
   | (ts, u) =>
       Syntax.const \<^syntax_const>\<open>_record_update\<close> $ u $
         foldr1 (fn (v, w) => Syntax.const \<^syntax_const>\<open>_field_updates\<close> $ v $ w) (rev ts));
 
 in
 
 fun field_update_tr' name =
   let
     val update_name = Lexicon.mark_const (name ^ updateN);
     fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
       | tr' _ _ = raise Match;
   in (update_name, tr') end;
 
 end;
 
 
 
 (** record simprocs **)
 
 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   (case get_updates thy u of
     SOME u_name => u_name = s
   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
 
 fun mk_comp_id f =
   let val T = range_type (fastype_of f)
   in HOLogic.mk_comp (\<^Const>\<open>id T\<close>, f) end;
 
 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   | get_upd_funs _ = [];
 
 fun get_accupd_simps ctxt term defset =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val (acc, [body]) = strip_comb term;
     val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
     fun get_simp upd =
       let
         (* FIXME fresh "f" (!?) *)
         val T = domain_type (fastype_of upd);
         val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
         val rhs =
           if is_sel_upd_pair thy acc upd
           then HOLogic.mk_comp (Free ("f", T), acc)
           else mk_comp_id acc;
         val prop = lhs === rhs;
         val othm =
           Goal.prove ctxt [] [] prop
             (fn {context = ctxt', ...} =>
               simp_tac (put_simpset defset ctxt') 1 THEN
               REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN
               TRY (simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms id_apply id_o o_id}) 1));
         val dest =
           if is_sel_upd_pair thy acc upd
           then @{thm o_eq_dest}
           else @{thm o_eq_id_dest};
       in Drule.export_without_context (othm RS dest) end;
   in map get_simp upd_funs end;
 
 fun get_updupd_simp ctxt defset u u' comp =
   let
     (* FIXME fresh "f" (!?) *)
     val f = Free ("f", domain_type (fastype_of u));
     val f' = Free ("f'", domain_type (fastype_of u'));
     val lhs = HOLogic.mk_comp (u $ f, u' $ f');
     val rhs =
       if comp
       then u $ HOLogic.mk_comp (f, f')
       else HOLogic.mk_comp (u' $ f', u $ f);
     val prop = lhs === rhs;
     val othm =
       Goal.prove ctxt [] [] prop
         (fn {context = ctxt', ...} =>
           simp_tac (put_simpset defset ctxt') 1 THEN
           REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN
           TRY (simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms id_apply}) 1));
     val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
   in Drule.export_without_context (othm RS dest) end;
 
 fun get_updupd_simps ctxt term defset =
   let
     val upd_funs = get_upd_funs term;
     val cname = fst o dest_Const;
     fun getswap u u' = get_updupd_simp ctxt defset u u' (cname u = cname u');
     fun build_swaps_to_eq _ [] swaps = swaps
       | build_swaps_to_eq upd (u :: us) swaps =
           let
             val key = (cname u, cname upd);
             val newswaps =
               if Symreltab.defined swaps key then swaps
               else Symreltab.insert (K true) (key, getswap u upd) swaps;
           in
             if cname u = cname upd then newswaps
             else build_swaps_to_eq upd us newswaps
           end;
     fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
       | swaps_needed (u :: us) prev seen swaps =
           if Symtab.defined seen (cname u)
           then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
           else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
 
 fun prove_unfold_defs thy ex_simps ex_simprs prop =
   let
     val ctxt = Proof_Context.init_global thy;
 
     val defset = get_sel_upd_defs thy;
     val prop' = Envir.beta_eta_contract prop;
     val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
     val (_, args) = strip_comb lhs;
     val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) ctxt lhs defset;
   in
     Goal.prove ctxt [] [] prop'
       (fn {context = ctxt', ...} =>
         simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ @{thms K_record_comp})) 1 THEN
         TRY (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ex_simps addsimprocs ex_simprs) 1))
   end;
 
 
 local
 
 fun eq (s1: string) (s2: string) = (s1 = s2);
 
 fun has_field extfields f T =
   exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
 
 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
       if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
   | K_skeleton n T b _ = ((n, T), b);
 
 in
 
 (* simproc *)
 
 (*
   Simplify selections of an record update:
     (1)  S (S_update k r) = k (S r)
     (2)  S (X_update k r) = S r
 
   The simproc skips multiple updates at once, eg:
    S (X_update x (Y_update y (S_update k r))) = k (S r)
 
   But be careful in (2) because of the extensibility of records.
   - If S is a more-selector we have to make sure that the update on component
     X does not affect the selected subrecord.
   - If X is a more-selector we have to make sure that S is not in the updated
     subrecord.
 *)
 val simproc =
   Simplifier.make_simproc \<^context> "record"
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
       in
         (case t of
           (sel as Const (s, Type (_, [_, rangeS]))) $
               ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
             if is_selector thy s andalso is_some (get_updates thy u) then
               let
                 val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
 
                 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
                       (case Symtab.lookup updates u of
                         NONE => NONE
                       | SOME u_name =>
                           if u_name = s then
                             (case mk_eq_terms r of
                               NONE =>
                                 let
                                   val rv = ("r", rT);
                                   val rb = Bound 0;
                                   val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
                                 in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
                             | SOME (trm, trm', vars) =>
                                 let
                                   val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
                                 in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
                           else if has_field extfields u_name rangeS orelse
                             has_field extfields s (domain_type kT) then NONE
                           else
                             (case mk_eq_terms r of
                               SOME (trm, trm', vars) =>
                                 let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
                                 in SOME (upd $ kb $ trm, trm', kv :: vars) end
                             | NONE =>
                                 let
                                   val rv = ("r", rT);
                                   val rb = Bound 0;
                                   val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
                                 in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
                   | mk_eq_terms _ = NONE;
               in
                 (case mk_eq_terms (upd $ k $ r) of
                   SOME (trm, trm', vars) =>
                     SOME
                       (prove_unfold_defs thy [] []
                         (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
                 | NONE => NONE)
               end
             else NONE
         | _ => NONE)
       end};
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
     val ctxt = Proof_Context.init_global thy;
     val prop =
       infer_instantiate ctxt
         [(("upd", 0), Thm.cterm_of ctxt upd), (("ac", 0), Thm.cterm_of ctxt acc)]
         updacc_cong_triv
       |> Thm.concl_of;
   in
     Goal.prove ctxt [] [] prop
       (fn {context = ctxt', ...} =>
         simp_tac (put_simpset ss ctxt') 1 THEN
         REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN
         TRY (resolve_tac ctxt' [updacc_cong_idI] 1))
   end;
 
 
 (* upd_simproc *)
 
 (*Simplify multiple updates:
     (1) "N_update y (M_update g (N_update x (M_update f r))) =
           (N_update (y o x) (M_update (g o f) r))"
     (2)  "r(|M:= M r|) = r"
 
   In both cases "more" updates complicate matters: for this reason
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
 val upd_simproc =
   Simplifier.make_simproc \<^context> "record_upd"
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
         (*We can use more-updators with other updators as long
           as none of the other updators go deeper than any more
           updator. min here is the depth of the deepest other
           updator, max the depth of the shallowest more updator.*)
         fun include_depth (dep, true) (min, max) =
               if min <= dep
               then SOME (min, if dep <= max orelse max = ~1 then dep else max)
               else NONE
           | include_depth (dep, false) (min, max) =
               if dep <= max orelse max = ~1
               then SOME (if min <= dep then dep else min, max)
               else NONE;
 
         fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
               (case get_update_details u thy of
                 SOME (s, dep, ismore) =>
                   (case include_depth (dep, ismore) (min, max) of
                     SOME (min', max') =>
                       let val (us, bs, _) = getupdseq tm min' max'
                       in ((upd, s, f) :: us, bs, fastype_of term) end
                   | NONE => ([], term, HOLogic.unitT))
               | NONE => ([], term, HOLogic.unitT))
           | getupdseq term _ _ = ([], term, HOLogic.unitT);
 
         val (upds, base, baseT) = getupdseq t 0 ~1;
 
         fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
               if s = s' andalso null (loose_bnos tm')
                 andalso subst_bound (HOLogic.unit, tm') = tm
               then (true, Abs (n, T, Const (s', T') $ Bound 1))
               else (false, HOLogic.unit)
           | is_upd_noop _ _ _ = (false, HOLogic.unit);
 
         fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
           let
             val ss = get_sel_upd_defs thy;
             val uathm = get_upd_acc_cong_thm upd acc thy ss;
           in
            [Drule.export_without_context (uathm RS updacc_noopE),
             Drule.export_without_context (uathm RS updacc_noop_compE)]
           end;
 
         (*If f is constant then (f o g) = f.  We know that K_skeleton
           only returns constant abstractions thus when we see an
           abstraction we can discard inner updates.*)
         fun add_upd (f as Abs _) _ = [f]
           | add_upd f fs = (f :: fs);
 
         (*mk_updterm returns
           (orig-term-skeleton, simplified-skeleton,
             variables, duplicate-updates, simp-flag, noop-simps)
 
           where duplicate-updates is a table used to pass upward
           the list of update functions which can be composed
           into an update above them, simp-flag indicates whether
           any simplification was achieved, and noop-simps are
           used for eliminating case (2) defined above*)
         fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
               let
                 val (lhs, rhs, vars, dups, simp, noops) =
                   mk_updterm upds (Symtab.update (u, ()) above) term;
                 val (fvar, skelf) =
                   K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
                 val (isnoop, skelf') = is_upd_noop s f term;
                 val funT = domain_type T;
                 fun mk_comp_local (f, f') =
                   Const (\<^const_name>\<open>Fun.comp\<close>, funT --> funT --> funT) $ f $ f';
               in
                 if isnoop then
                   (upd $ skelf' $ lhs, rhs, vars,
                     Symtab.update (u, []) dups, true,
                     if Symtab.defined noops u then noops
                     else Symtab.update (u, get_noop_simps upd skelf') noops)
                 else if Symtab.defined above u then
                   (upd $ skelf $ lhs, rhs, fvar :: vars,
                     Symtab.map_default (u, []) (add_upd skelf) dups,
                     true, noops)
                 else
                   (case Symtab.lookup dups u of
                     SOME fs =>
                      (upd $ skelf $ lhs,
                       upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
                       fvar :: vars, dups, true, noops)
                   | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
               end
           | mk_updterm [] _ _ =
               (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
           | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
 
         val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
         val noops' = maps snd (Symtab.dest noops);
       in
         if simp then
           SOME
             (prove_unfold_defs thy noops' [simproc]
               (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
         else NONE
       end};
 
 end;
 
 
 (* eq_simproc *)
 
 (*Look up the most specific record-equality.
 
  Note on efficiency:
  Testing equality of records boils down to the test of equality of all components.
  Therefore the complexity is: #components * complexity for single component.
  Especially if a record has a lot of components it may be better to split up
  the record first and do simplification on that (split_simp_tac).
  e.g. r(|lots of updates|) = x
 
              eq_simproc          split_simp_tac
  Complexity: #components * #updates     #updates
 *)
 val eq_simproc =
   Simplifier.make_simproc \<^context> "record_eq"
    {lhss = [\<^term>\<open>r = s\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         \<^Const_>\<open>HOL.eq T for _ _\<close> =>
           (case rec_id ~1 T of
             "" => NONE
           | name =>
               (case get_equalities (Proof_Context.theory_of ctxt) name of
                 NONE => NONE
               | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
       | _ => NONE)};
 
 
 (* split_simproc *)
 
 (*Split quantified occurrences of records, for which P holds.  P can peek on the
   subterm starting at the quantified occurrence of the record (including the quantifier):
     P t = 0: do not split
     P t = ~1: completely split
     P t > 0: split up to given bound of record extensions.*)
 fun split_simproc P =
   Simplifier.make_simproc \<^context> "record_split"
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
           if quantifier = \<^const_name>\<open>Pure.all\<close> orelse
             quantifier = \<^const_name>\<open>All\<close> orelse
             quantifier = \<^const_name>\<open>Ex\<close>
           then
             (case rec_id ~1 T of
               "" => NONE
             | _ =>
                 let val split = P (Thm.term_of ct) in
                   if split <> 0 then
                     (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
                       NONE => NONE
                     | SOME (all_thm, All_thm, Ex_thm, _) =>
                         SOME
                           (case quantifier of
                             \<^const_name>\<open>Pure.all\<close> => all_thm
                           | \<^const_name>\<open>All\<close> => All_thm RS @{thm eq_reflection}
                           | \<^const_name>\<open>Ex\<close> => Ex_thm RS @{thm eq_reflection}
                           | _ => raise Fail "split_simproc"))
                   else NONE
                 end)
           else NONE
       | _ => NONE)};
 
 val ex_sel_eq_simproc =
   Simplifier.make_simproc \<^context> "ex_sel_eq"
    {lhss = [\<^term>\<open>Ex t\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
         fun mkeq (lr, T, (sel, Tsel), x) i =
           if is_selector thy sel then
             let
               val x' =
                 if not (Term.is_dependent x)
                 then Free ("x" ^ string_of_int i, range_type Tsel)
                 else raise TERM ("", [x]);
               val sel' = Const (sel, Tsel) $ Bound 0;
               val (l, r) = if lr then (sel', x') else (x', sel');
             in \<^Const>\<open>HOL.eq T for l r\<close> end
           else raise TERM ("", [Const (sel, Tsel)]);
 
         fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
               (true, T, (sel, Tsel), X)
           | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
               (false, T, (sel, Tsel), X)
           | dest_sel_eq _ = raise TERM ("", []);
       in
         (case t of
           \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
            (let
              val eq = mkeq (dest_sel_eq t) 0;
              val prop =
                Logic.list_all ([("r", T)],
                  Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
             in
               SOME (Goal.prove_sorry_global thy [] [] prop
                 (fn {context = ctxt', ...} =>
                   simp_tac (put_simpset (get_simpset thy) ctxt'
                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
             end handle TERM _ => NONE)
         | _ => NONE)
       end};
 
 
 (* split_simp_tac *)
 
 (*Split (and simplify) all records in the goal for which P holds.
   For quantified occurrences of a record
   P can peek on the whole subterm (including the quantifier); for free variables P
   can only peek on the variable itself.
   P t = 0: do not split
   P t = ~1: completely split
   P t > 0: split up to given bound of record extensions.*)
 fun split_simp_tac ctxt thms P = CSUBGOAL (fn (cgoal, i) =>
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val goal = Thm.term_of cgoal;
     val frees = filter (is_recT o #2) (Term.add_frees goal []);
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
           (s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse s = \<^const_name>\<open>Ex\<close>)
             andalso is_recT T
         | _ => false);
 
     fun mk_split_free_tac free induct_thm i =
       let
         val _ $ (_ $ Var (r, _)) = Thm.concl_of induct_thm;
         val thm = infer_instantiate ctxt [(r, Thm.cterm_of ctxt free)] induct_thm;
       in
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
         resolve_tac ctxt [thm] i THEN
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_rulify}) i
       end;
 
     val split_frees_tacs =
       frees |> map_filter (fn (x, T) =>
         (case rec_id ~1 T of
           "" => NONE
         | _ =>
             let
               val free = Free (x, T);
               val split = P free;
             in
               if split <> 0 then
                 (case get_splits thy (rec_id split T) of
                   NONE => NONE
                 | SOME (_, _, _, induct_thm) =>
                     SOME (mk_split_free_tac free induct_thm i))
               else NONE
             end));
 
     val simprocs = if has_rec goal then [split_simproc P] else [];
     val thms' = @{thms o_apply K_record_comp} @ thms;
   in
     EVERY split_frees_tacs THEN
     full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' addsimprocs simprocs) i
   end);
 
 
 (* split_tac *)
 
 (*Split all records in the goal, which are quantified by !! or ALL.*)
 fun split_tac ctxt = CSUBGOAL (fn (cgoal, i) =>
   let
     val goal = Thm.term_of cgoal;
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
           (s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close>) andalso is_recT T
         | _ => false);
 
     fun is_all (Const (\<^const_name>\<open>Pure.all\<close>, _) $ _) = ~1
       | is_all (Const (\<^const_name>\<open>All\<close>, _) $ _) = ~1
       | is_all _ = 0;
   in
     if has_rec goal then
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs [split_simproc is_all]) i
     else no_tac
   end);
 
 val _ =
   Theory.setup
     (map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]));
 
 
 (* wrapper *)
 
 val split_name = "record_split_tac";
 val split_wrapper = (split_name, fn ctxt => fn tac => split_tac ctxt ORELSE' tac);
 
 
 
 (** theory extender interface **)
 
 (* attributes *)
 
 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
 
 
 (* tactics *)
 
 (*Do case analysis / induction according to rule on last parameter of ith subgoal
   (or on s if there are no parameters).
   Instatiation of record variable (and predicate) in rule is calculated to
   avoid problems with higher order unification.*)
 fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
   let
     val g = Thm.term_of cgoal;
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
     val rule' = Thm.lift_rule cgoal rule;
     val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (Thm.prop_of rule')));
     (*ca indicates if rule is a case analysis or induction rule*)
     val (x, ca) =
       (case rev (drop (length params) ys) of
         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
           (hd (rev (Logic.strip_assums_hyp (hd (Thm.prems_of rule')))))))), true)
       | [x] => (head_of x, false));
     val rule'' =
       infer_instantiate ctxt
         (map (apsnd (Thm.cterm_of ctxt))
           (case rev params of
             [] =>
               (case AList.lookup (op =) (Term.add_frees g []) s of
                 NONE => error "try_param_tac: no such variable"
               | SOME T =>
                   [(#1 (dest_Var P), if ca then concl else lambda (Free (s, T)) concl),
                    (#1 (dest_Var x), Free (s, T))])
           | (_, T) :: _ =>
               [(#1 (dest_Var P),
                 fold_rev Term.abs params
                   (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
                (#1 (dest_Var x), fold_rev Term.abs params (Bound 0))])) rule';
   in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end);
 
 
 fun extension_definition overloaded name fields alphas zeta moreT more vars thy =
   let
     val ctxt = Proof_Context.init_global thy;
 
     val base_name = Long_Name.base_name name;
 
     val fieldTs = map snd fields;
     val fields_moreTs = fieldTs @ [moreT];
 
     val alphas_zeta = alphas @ [zeta];
 
     val ext_binding = Binding.name (suffix extN base_name);
     val ext_name = suffix extN name;
     val ext_tyco = suffix ext_typeN name;
     val extT = Type (ext_tyco, map TFree alphas_zeta);
     val ext_type = fields_moreTs ---> extT;
 
 
     (* the tree of new types that will back the record extension *)
 
     val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
 
     fun mk_iso_tuple (left, right) (thy, i) =
       let
         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
         val ((_, cons), thy') = thy
           |> Iso_Tuple_Support.add_iso_tuple_type overloaded
             (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
               (fastype_of left, fastype_of right);
       in
         (cons $ left $ right, (thy', i + 1))
       end;
 
     (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
     fun mk_even_iso_tuple [arg] = pair arg
       | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
 
     fun build_meta_tree_type i thy vars more =
       let val len = length vars in
         if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
         else if len > 16 then
           let
             fun group16 [] = []
               | group16 xs = take 16 xs :: group16 (drop 16 xs);
             val vars' = group16 vars;
             val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
           in
             build_meta_tree_type i' thy' composites more
           end
         else
           let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
           in (term, thy') end
       end;
 
     val _ = timing_msg ctxt "record extension preparing definitions";
 
 
     (* 1st stage part 1: introduce the tree of new types *)
 
     val (ext_body, typ_thy) = timeit_msg ctxt "record extension nested type def:" (fn () =>
       build_meta_tree_type 1 thy vars more);
 
 
     (* prepare declarations and definitions *)
 
     (* 1st stage part 2: define the ext constant *)
 
     fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
     val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
 
     val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () =>
       typ_thy
       |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
       |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]);
     val defs_ctxt = Proof_Context.init_global defs_thy;
 
 
     (* prepare propositions *)
 
     val _ = timing_msg ctxt "record extension preparing propositions";
     val vars_more = vars @ [more];
     val variants = map (fn Free (x, _) => x) vars_more;
     val ext = mk_ext vars_more;
     val s = Free (rN, extT);
     val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
 
     val inject_prop =  (* FIXME local x x' *)
       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
         HOLogic.mk_conj (HOLogic.eq_const extT $
           mk_ext vars_more $ mk_ext vars_more', \<^term>\<open>True\<close>)
         ===
         foldr1 HOLogic.mk_conj
           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [\<^term>\<open>True\<close>])
       end;
 
     val induct_prop = (fold_rev Logic.all vars_more (Trueprop (P $ ext)), Trueprop (P $ s));
 
     val split_meta_prop =  (* FIXME local P *)
       let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT)
       in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
 
     val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
       simplify (put_simpset HOL_ss defs_ctxt)
         (Goal.prove_sorry_global defs_thy [] [] inject_prop
           (fn {context = ctxt', ...} =>
             simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [ext_def]) 1 THEN
             REPEAT_DETERM
               (resolve_tac ctxt' @{thms refl_conj_eq} 1 ORELSE
                 Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE
                 resolve_tac ctxt' [refl] 1))));
 
 
     (*We need a surjection property r = (| f = f r, g = g r ... |)
       to prove other theorems. We haven't given names to the accessors
       f, g etc yet however, so we generate an ext structure with
       free variables as all arguments and allow the introduction tactic to
       operate on it as far as it can. We then use Drule.export_without_context
       to convert the free variables into unifiable variables and unify them with
       (roughly) the definition of the accessor.*)
     val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
       let
         val start =
           infer_instantiate defs_ctxt [(("y", 0), Thm.cterm_of defs_ctxt ext)] surject_assist_idE;
         val tactic1 =
           simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
           REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1;
         val tactic2 =
           REPEAT (resolve_tac defs_ctxt [surject_assistI] 1 THEN resolve_tac defs_ctxt [refl] 1);
         val [halfway] = Seq.list_of (tactic1 start);
         val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
       in
         surject
       end);
 
     val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_meta_prop
         (fn {context = ctxt', ...} =>
           EVERY1
            [resolve_tac ctxt' @{thms equal_intr_rule},
             Goal.norm_hhf_tac ctxt',
             eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt',
             resolve_tac ctxt' [@{thm prop_subst} OF [surject]],
             REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt']));
 
     val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
       let val (assm, concl) = induct_prop in
         Goal.prove_sorry_global defs_thy [] [assm] concl
           (fn {context = ctxt', prems, ...} =>
             cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
             resolve_tac ctxt' prems 2 THEN
             asm_simp_tac (put_simpset HOL_ss ctxt') 1)
       end);
 
     val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) =
       defs_thy
       |> Global_Theory.note_thmss ""
           [((Binding.name "ext_induct", []), [([induct], [])]),
            ((Binding.name "ext_inject", []), [([inject], [])]),
            ((Binding.name "ext_surjective", []), [([surject], [])]),
            ((Binding.name "ext_split", []), [([split_meta], [])])];
   in
     (((ext_name, ext_type), (ext_tyco, alphas_zeta),
       extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
   end;
 
 fun chunks [] [] = []
   | chunks [] xs = [xs]
   | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
 
 fun chop_last [] = error "chop_last: list should not be empty"
   | chop_last [x] = ([], x)
   | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
 
 fun subst_last _ [] = error "subst_last: list should not be empty"
   | subst_last s [_] = [s]
   | subst_last s (x :: xs) = x :: subst_last s xs;
 
 
 (* mk_recordT *)
 
 (*build up the record type from the current extension tpye extT and a list
   of parent extensions, starting with the root of the record hierarchy*)
 fun mk_recordT extT =
   fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
 
 
 (* code generation *)
 
 fun mk_random_eq tyco vs extN Ts =
   let
     (* FIXME local i etc. *)
     val size = \<^term>\<open>i::natural\<close>;
     fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>);
     val T = Type (tyco, map TFree vs);
     val Tm = termifyT T;
     val params = Name.invent_names Name.context "x" Ts;
     val lhs = HOLogic.mk_random T size;
     val tc = HOLogic.mk_return Tm \<^typ>\<open>Random.seed\<close>
       (HOLogic.mk_valtermify_app extN params T);
     val rhs =
       HOLogic.mk_ST
         (map (fn (v, T') =>
           ((HOLogic.mk_random T' size, \<^typ>\<open>Random.seed\<close>), SOME (v, termifyT T'))) params)
         tc \<^typ>\<open>Random.seed\<close> (SOME Tm, \<^typ>\<open>Random.seed\<close>);
   in
     (lhs, rhs)
   end
 
 fun mk_full_exhaustive_eq tyco vs extN Ts =
   let
     (* FIXME local i etc. *)
     val size = \<^term>\<open>i::natural\<close>;
     fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>);
     val T = Type (tyco, map TFree vs);
     val test_function = Free ("f", termifyT T --> \<^typ>\<open>(bool \<times> term list) option\<close>);
     val params = Name.invent_names Name.context "x" Ts;
     fun mk_full_exhaustive U = \<^Const>\<open>full_exhaustive_class.full_exhaustive U\<close>;
     val lhs = mk_full_exhaustive T $ test_function $ size;
     val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
     val rhs = fold_rev (fn (v, U) => fn cont =>
         mk_full_exhaustive U $ (lambda (Free (v, termifyT U)) cont) $ size) params tc;
   in
     (lhs, rhs)
   end;
 
 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
   let
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
   in
     thy
     |> Class.instantiation ([tyco], vs, sort)
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
 
 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
   let
     val algebra = Sign.classes_of thy;
     val has_inst = Sorts.has_instance algebra ext_tyco sort;
   in
     if has_inst then thy
     else
       (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
         SOME constrain =>
           instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
             ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
       | NONE => thy)
   end;
 
 fun add_code ext_tyco vs extT ext simps inject thy =
   if Config.get_global thy codegen then
     let
       val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>HOL.equal extT\<close>, \<^Const>\<open>HOL.eq extT\<close>));
       fun tac ctxt eq_def =
         Class.intro_classes_tac ctxt []
         THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
         THEN ALLGOALS (resolve_tac ctxt @{thms refl});
       fun mk_eq ctxt eq_def =
         rewrite_rule ctxt
           [Axclass.unoverload ctxt (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
       fun mk_eq_refl ctxt =
-        @{thm equal_refl}
-        |> Thm.instantiate
-          (TVars.make [(\<^tvar>\<open>?'a::equal\<close>, Thm.ctyp_of ctxt (Logic.varifyT_global extT))], Vars.empty)
+        \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt (Logic.varifyT_global extT)\<close> in
+          lemma (schematic) \<open>equal_class.equal x x \<longleftrightarrow> True\<close> by (rule equal_refl)\<close>
         |> Axclass.unoverload ctxt;
       val ensure_random_record = ensure_sort_record (\<^sort>\<open>random\<close>, mk_random_eq);
       val ensure_exhaustive_record =
         ensure_sort_record (\<^sort>\<open>full_exhaustive\<close>, mk_full_exhaustive_eq);
       fun add_code eq_def thy =
         let
           val ctxt = Proof_Context.init_global thy;
         in
           thy
           |> Code.declare_default_eqns_global [(mk_eq ctxt eq_def, true), (mk_eq_refl ctxt, false)]
         end;
     in
       thy
       |> Code.declare_datatype_global [ext]
       |> Code.declare_default_eqns_global (map (rpair true) simps)
       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
       |-> (fn (_, (_, eq_def)) =>
          Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
       |-> add_code
       |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
       |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
     end
   else thy;
 
 fun add_ctr_sugar ctr exhaust inject sel_thms =
   Ctr_Sugar.default_register_ctr_sugar_global (K true)
     {kind = Ctr_Sugar.Record, T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy,
      discs = [], selss = [], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject],
      distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
      case_distribs = [], split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [],
      disc_thmss = [], discIs = [], disc_eq_cases = [], sel_defs = [], sel_thmss = [sel_thms],
      distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
      split_sels = [], split_sel_asms = [], case_eq_ifs = []};
 
 fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
   | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
 
 fun add_spec_rule rule =
   let val head = head_of (lhs_of_equation (Thm.prop_of rule))
   in Spec_Rules.add_global Binding.empty Spec_Rules.equational [head] [rule] end;
 
 (* definition *)
 
 fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
   let
     val ctxt0 = Proof_Context.init_global thy0;
 
     val prefix = Binding.name_of binding;
     val name = Sign.full_name thy0 binding;
     val full = Sign.full_name_path thy0 prefix;
 
     val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
     val field_syntax = map #3 raw_fields;
 
     val parent_fields = maps #fields parents;
     val parent_chunks = map (length o #fields) parents;
     val parent_names = map fst parent_fields;
     val parent_types = map snd parent_fields;
     val parent_fields_len = length parent_fields;
     val parent_variants =
       Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
     val parent_vars = map2 (curry Free) parent_variants parent_types;
     val parent_len = length parents;
 
     val fields = map (apfst full) bfields;
     val names = map fst fields;
     val types = map snd fields;
     val alphas_fields = fold Term.add_tfreesT types [];
     val alphas_ext = inter (op =) alphas_fields alphas;
     val len = length fields;
     val variants =
       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
         (map (Binding.name_of o fst) bfields);
     val vars = map2 (curry Free) variants types;
     val named_vars = names ~~ vars;
     val idxms = 0 upto len;
 
     val all_fields = parent_fields @ fields;
     val all_types = parent_types @ types;
     val all_variants = parent_variants @ variants;
     val all_vars = parent_vars @ vars;
     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
 
     val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", \<^sort>\<open>type\<close>);
     val moreT = TFree zeta;
     val more = Free (moreN, moreT);
     val full_moreN = full (Binding.name moreN);
     val bfields_more = bfields @ [(Binding.name moreN, moreT)];
     val fields_more = fields @ [(full_moreN, moreT)];
     val named_vars_more = named_vars @ [(full_moreN, more)];
     val all_vars_more = all_vars @ [more];
     val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
 
 
     (* 1st stage: ext_thy *)
 
     val extension_name = full binding;
 
     val ((ext, (ext_tyco, vs),
         extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
       thy0
       |> Sign.qualified_path false binding
       |> extension_definition overloaded extension_name fields alphas_ext zeta moreT more vars;
     val ext_ctxt = Proof_Context.init_global ext_thy;
 
     val _ = timing_msg ext_ctxt "record preparing definitions";
     val Type extension_scheme = extT;
     val extension_name = unsuffix ext_typeN (fst extension_scheme);
     val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
     val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
     val extension_id = implode extension_names;
 
     fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
     val rec_schemeT0 = rec_schemeT 0;
 
     fun recT n =
       let val (c, Ts) = extension in
         mk_recordT (map #extension (drop n parents))
           (Type (c, subst_last HOLogic.unitT Ts))
       end;
     val recT0 = recT 0;
 
     fun mk_rec args n =
       let
         val (args', more) = chop_last args;
         fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
         fun build Ts =
           fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
       in
         if more = HOLogic.unit
         then build (map_range recT (parent_len + 1))
         else build (map_range rec_schemeT (parent_len + 1))
       end;
 
     val r_rec0 = mk_rec all_vars_more 0;
     val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
 
     fun r n = Free (rN, rec_schemeT n);
     val r0 = r 0;
     fun r_unit n = Free (rN, recT n);
     val r_unit0 = r_unit 0;
 
 
     (* print translations *)
 
     val record_ext_type_abbr_tr's =
       let
         val trname = hd extension_names;
         val last_ext = unsuffix ext_typeN (fst extension);
       in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
 
     val record_ext_type_tr's =
       let
         (*avoid conflict with record_type_abbr_tr's*)
         val trnames = if parent_len > 0 then [extension_name] else [];
       in map record_ext_type_tr' trnames end;
 
     val print_translation =
       map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
       record_ext_type_tr's @ record_ext_type_abbr_tr's;
 
 
     (* prepare declarations *)
 
     val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
     val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
     val make_decl = (makeN, all_types ---> recT0);
     val fields_decl = (fields_selN, types ---> Type extension);
     val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
     val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
 
 
     (* prepare definitions *)
 
     val ext_defs = ext_def :: map #ext_def parents;
 
     (*Theorems from the iso_tuple intros.
       By unfolding ext_defs from r_rec0 we create a tree of constructor
       calls (many of them Pair, but others as well). The introduction
       rules for update_accessor_eq_assist can unify two different ways
       on these constructors. If we take the complete result sequence of
       running a the introduction tactic, we get one theorem for each upd/acc
       pair, from which we can derive the bodies of our selector and
       updator and their convs.*)
     val (accessor_thms, updator_thms, upd_acc_cong_assists) =
       timeit_msg ext_ctxt "record getting tree access/updates:" (fn () =>
         let
           val r_rec0_Vars =
             let
               (*pick variable indices of 1 to avoid possible variable
                 collisions with existing variables in updacc_eq_triv*)
               fun to_Var (Free (c, T)) = Var ((c, 1), T);
             in mk_rec (map to_Var all_vars_more) 0 end;
 
           val init_thm =
             infer_instantiate ext_ctxt
               [(("v", 0), Thm.cterm_of ext_ctxt r_rec0),
                (("v'", 0), Thm.cterm_of ext_ctxt r_rec0_Vars)]
               updacc_eq_triv;
           val terminal =
             resolve_tac ext_ctxt [updacc_eq_idI] 1 THEN resolve_tac ext_ctxt [refl] 1;
           val tactic =
             simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
             REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac ext_ctxt 1 ORELSE terminal);
           val updaccs = Seq.list_of (tactic init_thm);
         in
           (updaccs RL [updacc_accessor_eqE],
            updaccs RL [updacc_updator_eqE],
            updaccs RL [updacc_cong_from_eq])
         end);
 
     fun lastN xs = drop parent_fields_len xs;
 
     (*selectors*)
     fun mk_sel_spec ((c, T), thm) =
       let
         val (acc $ arg, _) =
           HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
         val _ =
           if arg aconv r_rec0 then ()
           else raise TERM ("mk_sel_spec: different arg", [arg]);
       in
         Const (mk_selC rec_schemeT0 (c, T)) :== acc
       end;
     val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
 
     (*updates*)
     fun mk_upd_spec ((c, T), thm) =
       let
         val (upd $ _ $ arg, _) =
           HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
         val _ =
           if arg aconv r_rec0 then ()
           else raise TERM ("mk_sel_spec: different arg", [arg]);
       in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
     val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
 
     (*derived operations*)
     val make_spec =
       list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
         mk_rec (all_vars @ [HOLogic.unit]) 0;
     val fields_spec =
       list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
         mk_rec (all_vars @ [HOLogic.unit]) parent_len;
     val extend_spec =
       Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
         mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
     val truncate_spec =
       Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
         mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
 
 
     (* 2st stage: defs_thy *)
 
     val (((sel_defs, upd_defs), derived_defs), defs_thy) =
       timeit_msg ext_ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
         (fn () =>
           ext_thy
           |> Sign.print_translation print_translation
           |> Sign.restore_naming thy0
           |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
           |> Typedecl.abbrev_global
             (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0
           |> snd
           |> Sign.qualified_path false binding
           |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
             (sel_decls ~~ (field_syntax @ [NoSyn]))
           |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
             (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
           |> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) sel_specs
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name)))
             [make_spec, fields_spec, extend_spec, truncate_spec]);
     val defs_ctxt = Proof_Context.init_global defs_thy;
 
     (* prepare propositions *)
     val _ = timing_msg defs_ctxt "record preparing propositions";
     val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
     val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
     val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
 
     (*selectors*)
     val sel_conv_props =
       map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
 
     (*updates*)
     fun mk_upd_prop i (c, T) =
       let
         val x' =
           Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
         val n = parent_fields_len + i;
         val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
       in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
     val upd_conv_props = map2 mk_upd_prop idxms fields_more;
 
     (*induct*)
     val induct_scheme_prop =
       fold_rev Logic.all all_vars_more (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
     val induct_prop =
       (fold_rev Logic.all all_vars (Trueprop (P_unit $ r_rec_unit0)), Trueprop (P_unit $ r_unit0));
 
     (*surjective*)
     val surjective_prop =
       let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
       in r0 === mk_rec args 0 end;
 
     (*cases*)
     val cases_scheme_prop =
       (fold_rev Logic.all all_vars_more ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
 
     val cases_prop =
       fold_rev Logic.all all_vars ((r_unit0 === r_rec_unit0) ==> Trueprop C) ==> Trueprop C;
 
     (*split*)
     val split_meta_prop =
       let
         val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT);
       in
         Logic.mk_equals (Logic.all r0 (P $ r0), fold_rev Logic.all all_vars_more (P $ r_rec0))
       end;
 
     val split_object_prop =
       let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
       in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
 
     val split_ex_prop =
       let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
       in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
 
     (*equality*)
     val equality_prop =
       let
         val s' = Free (rN ^ "'", rec_schemeT0);
         fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
         val seleqs = map mk_sel_eq all_named_vars_more;
       in Logic.all r0 (Logic.all s' (Logic.list_implies (seleqs, r0 === s'))) end;
 
 
     (* 3rd stage: thms_thy *)
 
     val record_ss = get_simpset defs_thy;
     val sel_upd_ss =
       simpset_of
         (put_simpset record_ss defs_ctxt
           addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms));
 
     val (sel_convs, upd_convs) =
       timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () =>
         grouped 10 Par_List.map (fn prop =>
             Goal.prove_sorry_global defs_thy [] [] prop
               (fn {context = ctxt', ...} =>
                 ALLGOALS (asm_full_simp_tac (put_simpset sel_upd_ss ctxt'))))
           (sel_conv_props @ upd_conv_props))
       |> chop (length sel_conv_props);
 
     val (fold_congs, unfold_congs) = timeit_msg defs_ctxt "record upd fold/unfold congs:" (fn () =>
       let
         val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
         val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt addsimps symdefs;
         val ua_congs = map (Drule.export_without_context o simplify fold_ctxt) upd_acc_cong_assists;
       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end);
 
     val parent_induct = Option.map #induct_scheme (try List.last parents);
 
     val induct_scheme = timeit_msg defs_ctxt "record induct_scheme proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
         (fn {context = ctxt', ...} =>
           EVERY
            [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt' rN ind 1,
             try_param_tac ctxt' rN ext_induct 1,
             asm_simp_tac (put_simpset HOL_basic_ss ctxt') 1]));
 
     val induct = timeit_msg defs_ctxt "record induct proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop)
         (fn {context = ctxt', prems, ...} =>
           try_param_tac ctxt' rN induct_scheme 1
           THEN try_param_tac ctxt' "more" @{thm unit.induct} 1
           THEN resolve_tac ctxt' prems 1));
 
     val surjective = timeit_msg defs_ctxt "record surjective proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] surjective_prop
         (fn {context = ctxt', ...} =>
           EVERY
            [resolve_tac ctxt' [surject_assist_idE] 1,
             simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ext_defs) 1,
             REPEAT
               (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE
                 (resolve_tac ctxt' [surject_assistI] 1 THEN
                   simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt'
                     addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))]));
 
     val cases_scheme = timeit_msg defs_ctxt "record cases_scheme proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
         (fn {context = ctxt', prems, ...} =>
           resolve_tac ctxt' prems 1 THEN
           resolve_tac ctxt' [surjective] 1));
 
     val cases = timeit_msg defs_ctxt "record cases proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] cases_prop
         (fn {context = ctxt', ...} =>
           try_param_tac ctxt' rN cases_scheme 1 THEN
           ALLGOALS (asm_full_simp_tac
             (put_simpset HOL_basic_ss ctxt' addsimps @{thms unit_all_eq1}))));
 
     val split_meta = timeit_msg defs_ctxt "record split_meta proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_meta_prop
         (fn {context = ctxt', ...} =>
           EVERY1
            [resolve_tac ctxt' @{thms equal_intr_rule}, Goal.norm_hhf_tac ctxt',
             eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt',
             resolve_tac ctxt' [@{thm prop_subst} OF [surjective]],
             REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt']));
 
     val split_object = timeit_msg defs_ctxt "record split_object proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_object_prop
         (fn {context = ctxt', ...} =>
           resolve_tac ctxt' [@{lemma "Trueprop A \<equiv> Trueprop B \<Longrightarrow> A = B" by (rule iffI) unfold}] 1 THEN
           rewrite_goals_tac ctxt' @{thms atomize_all [symmetric]} THEN
           resolve_tac ctxt' [split_meta] 1));
 
     val split_ex = timeit_msg defs_ctxt "record split_ex proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_ex_prop
         (fn {context = ctxt', ...} =>
           simp_tac
             (put_simpset HOL_basic_ss ctxt' addsimps
               (@{lemma "\<exists>x. P x \<equiv> \<not> (\<forall>x. \<not> P x)" by simp} ::
                 @{thms not_not Not_eq_iff})) 1 THEN
           resolve_tac ctxt' [split_object] 1));
 
     val equality = timeit_msg defs_ctxt "record equality proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] equality_prop
         (fn {context = ctxt', ...} =>
           asm_full_simp_tac (put_simpset record_ss ctxt' addsimps (split_meta :: sel_convs)) 1));
 
     val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
           (_, fold_congs'), (_, unfold_congs'),
           (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'),
           (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']),
           (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy
       |> Code.declare_default_eqns_global (map (rpair true) derived_defs)
       |> Global_Theory.note_thmss ""
        [((Binding.name "select_convs", []), [(sel_convs, [])]),
         ((Binding.name "update_convs", []), [(upd_convs, [])]),
         ((Binding.name "select_defs", []), [(sel_defs, [])]),
         ((Binding.name "update_defs", []), [(upd_defs, [])]),
         ((Binding.name "fold_congs", []), [(fold_congs, [])]),
         ((Binding.name "unfold_congs", []), [(unfold_congs, [])]),
         ((Binding.name "splits", []), [([split_meta, split_object, split_ex], [])]),
         ((Binding.name "defs", []), [(derived_defs, [])]),
         ((Binding.name "surjective", []), [([surjective], [])]),
         ((Binding.name "equality", []), [([equality], [])]),
         ((Binding.name "induct_scheme", induct_type_global (suffix schemeN name)),
           [([induct_scheme], [])]),
         ((Binding.name "induct", induct_type_global name), [([induct], [])]),
         ((Binding.name "cases_scheme", cases_type_global (suffix schemeN name)),
           [([cases_scheme], [])]),
         ((Binding.name "cases", cases_type_global name), [([cases], [])])];
 
     val sel_upd_simps = sel_convs' @ upd_convs';
     val sel_upd_defs = sel_defs' @ upd_defs';
     val depth = parent_len + 1;
 
     val ([(_, simps'), (_, iffs')], thms_thy') = thms_thy
       |> Global_Theory.note_thmss ""
           [((Binding.name "simps", [Simplifier.simp_add]), [(sel_upd_simps, [])]),
            ((Binding.name "iffs", [iff_add]), [([ext_inject], [])])];
 
     val info =
       make_info alphas parent fields extension
         ext_induct ext_inject ext_surjective ext_split ext_def
         sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
         surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
 
     val final_thy =
       thms_thy'
       |> put_record name info
       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs
       |> add_equalities extension_id equality'
       |> add_extinjects ext_inject
       |> add_extsplit extension_name ext_split
       |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
       |> add_fieldext (extension_name, snd extension) names
       |> add_code ext_tyco vs extT ext simps' ext_inject
       |> add_ctr_sugar (Const ext) cases_scheme' ext_inject sel_convs'
       |> fold add_spec_rule (sel_convs' @ upd_convs' @ derived_defs')
       |> Sign.restore_naming thy0;
 
   in final_thy end;
 
 
 (* add_record *)
 
 local
 
 fun read_parent NONE ctxt = (NONE, ctxt)
   | read_parent (SOME raw_T) ctxt =
       (case Proof_Context.read_typ_abbrev ctxt raw_T of
         Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
       | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
 
 fun read_fields raw_fields ctxt =
   let
     val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
     val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
     val ctxt' = fold Variable.declare_typ Ts ctxt;
   in (fields, ctxt') end;
 
 in
 
 fun add_record overloaded (params, binding) raw_parent raw_fields thy =
   let
     val ctxt = Proof_Context.init_global thy;
     fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
       handle TYPE (msg, _, _) => error msg;
 
 
     (* specification *)
 
     val parent = Option.map (apfst (map cert_typ)) raw_parent
       handle ERROR msg =>
         cat_error msg ("The error(s) above occurred in parent record specification");
     val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
     val parents = get_parent_info thy parent;
 
     val bfields =
       raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx)
         handle ERROR msg =>
           cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x));
 
 
     (* errors *)
 
     val name = Sign.full_name thy binding;
     val err_dup_record =
       if is_none (get_info thy name) then []
       else ["Duplicate definition of record " ^ quote name];
 
     val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
     val err_extra_frees =
       (case subtract (op =) params spec_frees of
         [] => []
       | extras => ["Extra free type variable(s) " ^
           commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
 
     val err_no_fields = if null bfields then ["No fields present"] else [];
 
     val err_dup_fields =
       (case duplicates Binding.eq_name (map #1 bfields) of
         [] => []
       | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
 
     val err_bad_fields =
       if forall (not_equal moreN o Binding.name_of o #1) bfields then []
       else ["Illegal field name " ^ quote moreN];
 
     val errs =
       err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
     val _ = if null errs then () else error (cat_lines errs);
   in
     thy |> definition overloaded (params, binding) parent parents bfields
   end
   handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
 
 fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
     val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
     val (parent, ctxt2) = read_parent raw_parent ctxt1;
     val (fields, ctxt3) = read_fields raw_fields ctxt2;
     val params' = map (Proof_Context.check_tfree ctxt3) params;
   in thy |> add_record overloaded (params', binding) parent fields end;
 
 end;
 
 
 (* printing *)
 
 local
 
 fun the_parent_recT (Type (parent, [Type (_, [unit as Type (_,[])])])) = Type (parent, [unit])
   | the_parent_recT (Type (extT, [T])) = Type (extT, [the_parent_recT T])
   | the_parent_recT T = raise TYPE ("Not a unit record scheme with parent: ", [T], [])
 
 in
 
 fun pretty_recT ctxt typ =
   let
     val thy = Proof_Context.theory_of ctxt
     val (fs, (_, moreT)) = get_recT_fields thy typ
     val _ = if moreT = HOLogic.unitT then () else raise TYPE ("Not a unit record scheme: ", [typ], [])
     val parent = if length (dest_recTs typ) >= 2 then SOME (the_parent_recT typ) else NONE
     val pfs = case parent of SOME p => fst (get_recT_fields thy p) | NONE => []
     val fs' = drop (length pfs) fs
     fun pretty_field (name, typ) = Pretty.block [
           Syntax.pretty_term ctxt (Const (name, typ)),
           Pretty.brk 1,
           Pretty.str "::",
           Pretty.brk 1,
           Syntax.pretty_typ ctxt typ
         ]
   in
     Pretty.block (Library.separate (Pretty.brk 1)
       ([Pretty.keyword1 "record", Syntax.pretty_typ ctxt typ, Pretty.str "="] @
         (case parent of
           SOME p => [Syntax.pretty_typ ctxt p, Pretty.str "+"]
         | NONE => [])) @
       Pretty.fbrk ::
       Pretty.fbreaks (map pretty_field fs'))
   end
 
 end
 
 fun string_of_record ctxt s =
   let
     val T = Syntax.read_typ ctxt s
   in
     Pretty.string_of (pretty_recT ctxt T)
       handle TYPE _ => error ("Unknown record: " ^ Syntax.string_of_typ ctxt T)
   end
 
 val print_record =
   let
     fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
          Print_Mode.with_modes modes (fn () => Output.writeln (string_of state arg)) ());
   in print_item (string_of_record o Toplevel.context_of) end
 
 
 (* outer syntax *)
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>record\<close> "define extensible record"
     (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) --
       (\<^keyword>\<open>=\<close> |-- Scan.option (Parse.typ --| \<^keyword>\<open>+\<close>) --
         Scan.repeat1 Parse.const_binding)
     >> (fn ((overloaded, x), (y, z)) =>
         Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
 
 val opt_modes =
   Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) []
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_record\<close> "print record definiton"
     (opt_modes -- Parse.typ >> print_record);
 
 end
diff --git a/src/HOL/Tools/sat.ML b/src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML
+++ b/src/HOL/Tools/sat.ML
@@ -1,470 +1,468 @@
 (*  Title:      HOL/Tools/sat.ML
     Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     Author:     Tjark Weber, TU Muenchen
 
 Proof reconstruction from SAT solvers.
 
   Description:
     This file defines several tactics to invoke a proof-producing
     SAT solver on a propositional goal in clausal form.
 
     We use a sequent presentation of clauses to speed up resolution
     proof reconstruction.
     We call such clauses "raw clauses", which are of the form
           [x1, ..., xn, P] |- False
     (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
     where each xi is a literal (see also comments in cnf.ML).
 
     This does not work for goals containing schematic variables!
 
       The tactic produces a clause representation of the given goal
       in DIMACS format and invokes a SAT solver, which should return
       a proof consisting of a sequence of resolution steps, indicating
       the two input clauses, and resulting in new clauses, leading to
       the empty clause (i.e. "False").  The tactic replays this proof
       in Isabelle and thus solves the overall goal.
 
   There are three SAT tactics available.  They differ in the CNF transformation
   used. "sat_tac" uses naive CNF transformation to transform the theorem to be
   proved before giving it to the SAT solver.  The naive transformation in the
   worst case can lead to an exponential blow up in formula size.  Another
   tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
   produce a formula of linear size increase compared to the input formula, at
   the cost of possibly introducing new variables.  See cnf.ML for more
   comments on the CNF transformation.  "rawsat_tac" should be used with
   caution: no CNF transformation is performed, and the tactic's behavior is
   undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
   where each Ci is a disjunction.
 
   The SAT solver to be used can be set via the "solver" reference.  See
   sat_solvers.ML for possible values, and etc/settings for required (solver-
   dependent) configuration settings.  To replay SAT proofs in Isabelle, you
   must of course use a proof-producing SAT solver in the first place.
 
   Proofs are replayed only if "quick_and_dirty" is false.  If
   "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
   negation to be unsatisfiable) is proved via an oracle.
 *)
 
 signature SAT =
 sig
   val trace: bool Config.T  (* print trace messages *)
   val solver: string Config.T  (* name of SAT solver to be used *)
   val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
   val rawsat_thm: Proof.context -> cterm list -> thm
   val rawsat_tac: Proof.context -> int -> tactic
   val sat_tac: Proof.context -> int -> tactic
   val satx_tac: Proof.context -> int -> tactic
 end
 
 structure SAT : SAT =
 struct
 
 val trace = Attrib.setup_config_bool \<^binding>\<open>sat_trace\<close> (K false);
 
 fun cond_tracing ctxt msg =
   if Config.get ctxt trace then tracing (msg ()) else ();
 
 val solver = Attrib.setup_config_string \<^binding>\<open>sat_solver\<close> (K "cdclite");
   (*see HOL/Tools/sat_solver.ML for possible values*)
 
 val counter = Unsynchronized.ref 0;
 
-val resolution_thm =
-  @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False" by (rule case_split)}
-
 (* ------------------------------------------------------------------------- *)
 (* lit_ord: an order on integers that considers their absolute values only,  *)
 (*      thereby treating integers that represent the same atom (positively   *)
 (*      or negatively) as equal                                              *)
 (* ------------------------------------------------------------------------- *)
 
 fun lit_ord (i, j) = int_ord (abs i, abs j);
 
 (* ------------------------------------------------------------------------- *)
 (* CLAUSE: during proof reconstruction, three kinds of clauses are           *)
 (*      distinguished:                                                       *)
 (*      1. NO_CLAUSE: clause not proved (yet)                                *)
 (*      2. ORIG_CLAUSE: a clause as it occurs in the original problem        *)
 (*      3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
 (*         (a mapping from int's to its literals) for faster proof           *)
 (*         reconstruction                                                    *)
 (* ------------------------------------------------------------------------- *)
 
 datatype CLAUSE =
     NO_CLAUSE
   | ORIG_CLAUSE of thm
   | RAW_CLAUSE of thm * (int * cterm) list;
 
 (* ------------------------------------------------------------------------- *)
 (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
 (*      resolution over the list (starting with its head), i.e. with two raw *)
 (*      clauses                                                              *)
 (*        [P, x1, ..., a, ..., xn] |- False                                  *)
 (*      and                                                                  *)
 (*        [Q, y1, ..., a', ..., ym] |- False                                 *)
 (*      (where a and a' are dual to each other), we convert the first clause *)
 (*      to                                                                   *)
 (*        [P, x1, ..., xn] |- a ==> False ,                                  *)
 (*      the second clause to                                                 *)
 (*        [Q, y1, ..., ym] |- a' ==> False                                   *)
 (*      and then perform resolution with                                     *)
 (*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
 (*      to produce                                                           *)
 (*        [P, Q, x1, ..., xn, y1, ..., ym] |- False                          *)
 (*      Each clause is accompanied with an association list mapping integers *)
 (*      (positive for positive literals, negative for negative literals, and *)
 (*      the same absolute value for dual literals) to the actual literals as *)
 (*      cterms.                                                              *)
 (* ------------------------------------------------------------------------- *)
 
 fun resolve_raw_clauses _ [] =
       raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
   | resolve_raw_clauses ctxt (c::cs) =
       let
         (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
         fun merge xs [] = xs
           | merge [] ys = ys
           | merge (x :: xs) (y :: ys) =
               (case lit_ord (apply2 fst (x, y)) of
                 LESS => x :: merge xs (y :: ys)
               | EQUAL => x :: merge xs ys
               | GREATER => y :: merge (x :: xs) ys)
 
         (* find out which two hyps are used in the resolution *)
         fun find_res_hyps ([], _) _ =
               raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
           | find_res_hyps (_, []) _ =
               raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
           | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
               (case lit_ord  (apply2 fst (h1, h2)) of
                 LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
               | EQUAL =>
                   let
                     val (i1, chyp1) = h1
                     val (i2, chyp2) = h2
                   in
                     if i1 = ~ i2 then
                       (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
                     else (* i1 = i2 *)
                       find_res_hyps (hyps1, hyps2) (h1 :: acc)
                   end
           | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
 
         fun resolution (c1, hyps1) (c2, hyps2) =
           let
             val _ =
               cond_tracing ctxt (fn () =>
                 "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^
                 " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
                 ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^
                 " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
 
             (* the two literals used for resolution *)
             val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
 
             val c1' = Thm.implies_intr hyp1 c1  (* Gamma1 |- hyp1 ==> False *)
             val c2' = Thm.implies_intr hyp2 c2  (* Gamma2 |- hyp2 ==> False *)
 
-            val res_thm =  (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
+            val res_thm =
               let
-                val cLit =
+                val P =
                   snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1))  (* strip Trueprop *)
               in
-                Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, cLit)]) resolution_thm
+                \<^instantiate>\<open>P in
+                  lemma \<open>(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False\<close> by (rule case_split)\<close>
               end
 
             val _ =
               cond_tracing ctxt
                 (fn () => "Resolution theorem: " ^ Thm.string_of_thm ctxt res_thm)
 
             (* Gamma1, Gamma2 |- False *)
             val c_new =
               Thm.implies_elim
                 (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
                 (if hyp1_is_neg then c1' else c2')
 
             val _ =
               cond_tracing ctxt (fn () =>
                 "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^
                 " (hyps: " ^
                 ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
 
             val _ = Unsynchronized.inc counter
           in
             (c_new, new_hyps)
           end
         in
           fold resolution cs c
         end;
 
 (* ------------------------------------------------------------------------- *)
 (* replay_proof: replays the resolution proof returned by the SAT solver;    *)
 (*      cf. SAT_Solver.proof for details of the proof format.  Updates the   *)
 (*      'clauses' array with derived clauses, and returns the derived clause *)
 (*      at index 'empty_id' (which should just be "False" if proof           *)
 (*      reconstruction was successful, with the used clauses as hyps).       *)
 (*      'atom_table' must contain an injective mapping from all atoms that   *)
 (*      occur (as part of a literal) in 'clauses' to positive integers.      *)
 (* ------------------------------------------------------------------------- *)
 
 fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
   let
     fun index_of_literal chyp =
       (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
         (Const (\<^const_name>\<open>Not\<close>, _) $ atom) =>
           SOME (~ (the (Termtab.lookup atom_table atom)))
       | atom => SOME (the (Termtab.lookup atom_table atom)))
       handle TERM _ => NONE;  (* 'chyp' is not a literal *)
 
     fun prove_clause id =
       (case Array.sub (clauses, id) of
         RAW_CLAUSE clause => clause
       | ORIG_CLAUSE thm =>
           (* convert the original clause *)
           let
             val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
             val raw = CNF.clause2raw_thm ctxt thm
             val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
               Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw))
             val clause = (raw, hyps)
             val _ = Array.update (clauses, id, RAW_CLAUSE clause)
           in
             clause
           end
       | NO_CLAUSE =>
           (* prove the clause, using information from 'clause_table' *)
           let
             val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...")
             val ids = the (Inttab.lookup clause_table id)
             val clause = resolve_raw_clauses ctxt (map prove_clause ids)
             val _ = Array.update (clauses, id, RAW_CLAUSE clause)
             val _ =
               cond_tracing ctxt
                 (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id)
           in
             clause
           end)
 
     val _ = counter := 0
     val empty_clause = fst (prove_clause empty_id)
     val _ =
       cond_tracing ctxt (fn () =>
         "Proof reconstruction successful; " ^
         string_of_int (!counter) ^ " resolution step(s) total.")
   in
     empty_clause
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* string_of_prop_formula: return a human-readable string representation of  *)
 (*      a 'prop_formula' (just for tracing)                                  *)
 (* ------------------------------------------------------------------------- *)
 
 fun string_of_prop_formula Prop_Logic.True = "True"
   | string_of_prop_formula Prop_Logic.False = "False"
   | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
   | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
   | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
       "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
   | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
       "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
 
 (* ------------------------------------------------------------------------- *)
 (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
 (*      a proof from the resulting proof trace of the SAT solver.  The       *)
 (*      theorem returned is just "False" (with some of the given clauses as  *)
 (*      hyps).                                                               *)
 (* ------------------------------------------------------------------------- *)
 
 fun rawsat_thm ctxt clauses =
   let
     (* remove premises that equal "True" *)
     val clauses' = filter (fn clause =>
       (not_equal \<^term>\<open>True\<close> o HOLogic.dest_Trueprop o Thm.term_of) clause
         handle TERM ("dest_Trueprop", _) => true) clauses
     (* remove non-clausal premises -- of course this shouldn't actually   *)
     (* remove anything as long as 'rawsat_tac' is only called after the   *)
     (* premises have been converted to clauses                            *)
     val clauses'' = filter (fn clause =>
       ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
         handle TERM ("dest_Trueprop", _) => false)
       orelse
        (if Context_Position.is_visible ctxt then
           warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause))
         else (); false)) clauses'
     (* remove trivial clauses -- this is necessary because zChaff removes *)
     (* trivial clauses during preprocessing, and otherwise our clause     *)
     (* numbering would be off                                             *)
     val nontrivial_clauses =
       filter (not o CNF.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
     (* sort clauses according to the term order -- an optimization,       *)
     (* useful because forming the union of hypotheses, as done by         *)
     (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
     (* terms sorted in descending order, while only linear for terms      *)
     (* sorted in ascending order                                          *)
     val sorted_clauses = sort Thm.fast_term_ord nontrivial_clauses
     val _ =
       cond_tracing ctxt (fn () =>
         "Sorted non-trivial clauses:\n" ^
         cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
     (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
     val (fms, atom_table) =
       fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
         sorted_clauses Termtab.empty
     val _ =
       cond_tracing ctxt
         (fn () => "Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
     val fm = Prop_Logic.all fms
     fun make_quick_and_dirty_thm () =
       let
         val _ =
           cond_tracing ctxt
             (fn () => "quick_and_dirty is set: proof reconstruction skipped, using oracle instead")
         val False_thm = Skip_Proof.make_thm_cterm \<^cprop>\<open>False\<close>
       in
         (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
         (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
         (* clauses in ascending order (which is linear for                  *)
         (* 'Conjunction.intr_balanced', used below)                         *)
         fold Thm.weaken (rev sorted_clauses) False_thm
       end
   in
     case
       let
         val the_solver = Config.get ctxt solver
         val _ = cond_tracing ctxt (fn () => "Invoking solver " ^ the_solver)
       in SAT_Solver.invoke_solver the_solver fm end
     of
       SAT_Solver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
        (cond_tracing ctxt (fn () =>
           "Proof trace from SAT solver:\n" ^
           "clauses: " ^ ML_Syntax.print_list
             (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
             (Inttab.dest clause_table) ^ "\n" ^
           "empty clause: " ^ string_of_int empty_id);
         if Config.get ctxt quick_and_dirty then
           make_quick_and_dirty_thm ()
         else
           let
             (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
             (*               this avoids accumulation of hypotheses during resolution    *)
             (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
             val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
             (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
             val cnf_cterm = Thm.cprop_of clauses_thm
             val cnf_thm = Thm.assume cnf_cterm
             (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
             val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
             (* initialize the clause array with the given clauses *)
             val max_idx = fst (the (Inttab.max clause_table))
             val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
             val _ =
               fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
                 cnf_clauses 0
             (* replay the proof to derive the empty clause *)
             (* [c_1 && ... && c_n] |- False *)
             val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
           in
             (* [c_1, ..., c_n] |- False *)
             Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
           end)
     | SAT_Solver.UNSATISFIABLE NONE =>
         if Config.get ctxt quick_and_dirty then
          (if Context_Position.is_visible ctxt then
             warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"
           else ();
           make_quick_and_dirty_thm ())
         else
           raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
     | SAT_Solver.SATISFIABLE assignment =>
         let
           val msg =
             "SAT solver found a countermodel:\n" ^
             (commas o map (fn (term, idx) =>
                 Syntax.string_of_term_global \<^theory> term ^ ": " ^
                   (case assignment idx of NONE => "arbitrary"
                   | SOME true => "true" | SOME false => "false")))
               (Termtab.dest atom_table)
         in
           raise THM (msg, 0, [])
         end
     | SAT_Solver.UNKNOWN =>
         raise THM ("SAT solver failed to decide the formula", 0, [])
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* Tactics                                                                   *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
 (* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal      *)
 (*      should be of the form                                                *)
 (*        [| c1; c2; ...; ck |] ==> False                                    *)
 (*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
 (*      or "True"                                                            *)
 (* ------------------------------------------------------------------------- *)
 
 fun rawsat_tac ctxt i =
   Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
     resolve_tac ctxt' [rawsat_thm ctxt' (map Thm.cprop_of prems)] 1) ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* pre_cnf_tac: converts the i-th subgoal                                    *)
 (*        [| A1 ; ... ; An |] ==> B                                          *)
 (*      to                                                                   *)
 (*        [| A1; ... ; An ; ~B |] ==> False                                  *)
 (*      (handling meta-logical connectives in B properly before negating),   *)
 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
 (*      "-->", "!", and "="), then performs beta-eta-normalization on the    *)
 (*      subgoal                                                              *)
 (* ------------------------------------------------------------------------- *)
 
 fun pre_cnf_tac ctxt =
   resolve_tac ctxt @{thms ccontr} THEN'
   Object_Logic.atomize_prems_tac ctxt THEN'
   CONVERSION Drule.beta_eta_conversion;
 
 (* ------------------------------------------------------------------------- *)
 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
 (*      if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
 (*      becomes a separate premise), then applies 'rawsat_tac' to solve the  *)
 (*      subgoal                                                              *)
 (* ------------------------------------------------------------------------- *)
 
 fun cnfsat_tac ctxt i =
   (eresolve_tac  ctxt [FalseE] i) ORELSE
   (REPEAT_DETERM (eresolve_tac ctxt [conjE] i) THEN rawsat_tac ctxt i);
 
 (* ------------------------------------------------------------------------- *)
 (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
 (*      premises; if not, eliminates conjunctions (i.e. each clause of the   *)
 (*      CNF formula becomes a separate premise) and existential quantifiers, *)
 (*      then applies 'rawsat_tac' to solve the subgoal                       *)
 (* ------------------------------------------------------------------------- *)
 
 fun cnfxsat_tac ctxt i =
   (eresolve_tac ctxt [FalseE] i) ORELSE
     (REPEAT_DETERM (eresolve_tac ctxt [conjE] i ORELSE eresolve_tac ctxt [exE] i) THEN
       rawsat_tac ctxt i);
 
 (* ------------------------------------------------------------------------- *)
 (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
 (*      arbitrary formula.  The input is translated to CNF, possibly causing *)
 (*      an exponential blowup.                                               *)
 (* ------------------------------------------------------------------------- *)
 
 fun sat_tac ctxt i =
   pre_cnf_tac ctxt i THEN CNF.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
 
 (* ------------------------------------------------------------------------- *)
 (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
 (*      arbitrary formula.  The input is translated to CNF, possibly         *)
 (*      introducing new literals.                                            *)
 (* ------------------------------------------------------------------------- *)
 
 fun satx_tac ctxt i =
   pre_cnf_tac ctxt i THEN CNF.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
 
 end;