merged
authorberghofe
Tue Jun 01 11:30:57 2010 +0200 (2010-06-01 ago)
changeset 37236739d8b9c59da
parent 37225 32c5251f78cd
parent 37235 cafcc42bae77
child 37237 957753a47670
merged
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/Isar/class_target.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/proofterm.ML
src/Pure/type_infer.ML
     1.1 --- a/src/HOL/Extraction.thy	Tue Jun 01 11:18:51 2010 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Tue Jun 01 11:30:57 2010 +0200
     1.3 @@ -18,7 +18,8 @@
     1.4        Proofterm.rewrite_proof_notypes
     1.5          ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
     1.6        Proofterm.rewrite_proof thy
     1.7 -        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
     1.8 +        (RewriteHOLProof.rews,
     1.9 +         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
    1.10        ProofRewriteRules.elim_vars (curry Const @{const_name default}))
    1.11  *}
    1.12  
    1.13 @@ -199,223 +200,212 @@
    1.14  theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
    1.15    (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
    1.16  
    1.17 -setup {*
    1.18 -  Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"})
    1.19 -*}
    1.20 -
    1.21  realizers
    1.22    impI (P, Q): "\<lambda>pq. pq"
    1.23 -    "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.24 +    "\<Lambda> (c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.25  
    1.26    impI (P): "Null"
    1.27 -    "\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.28 +    "\<Lambda> (c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.29  
    1.30 -  impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _"
    1.31 +  impI (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. impI \<cdot> _ \<cdot> _"
    1.32  
    1.33    impI: "Null" "impI"
    1.34  
    1.35    mp (P, Q): "\<lambda>pq. pq"
    1.36 -    "\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
    1.37 +    "\<Lambda> (c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
    1.38  
    1.39    mp (P): "Null"
    1.40 -    "\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
    1.41 +    "\<Lambda> (c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
    1.42  
    1.43 -  mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _"
    1.44 +  mp (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. mp \<cdot> _ \<cdot> _"
    1.45  
    1.46    mp: "Null" "mp"
    1.47  
    1.48 -  allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _"
    1.49 +  allI (P): "\<lambda>p. p" "\<Lambda> (c: _) P (d: _) p. allI \<cdot> _ \<bullet> d"
    1.50  
    1.51    allI: "Null" "allI"
    1.52  
    1.53 -  spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x"
    1.54 +  spec (P): "\<lambda>x p. p x" "\<Lambda> (c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d"
    1.55  
    1.56    spec: "Null" "spec"
    1.57  
    1.58 -  exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x"
    1.59 +  exI (P): "\<lambda>x p. (x, p)" "\<Lambda> (c: _) P x (d: _) p. exI_realizer \<cdot> P \<cdot> p \<cdot> x \<bullet> c \<bullet> d"
    1.60  
    1.61 -  exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h"
    1.62 +  exI: "\<lambda>x. x" "\<Lambda> P x (c: _) (h: _). h"
    1.63  
    1.64    exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y"
    1.65 -    "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
    1.66 +    "\<Lambda> (c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> c \<bullet> e \<bullet> d \<bullet> h"
    1.67  
    1.68    exE (P): "Null"
    1.69 -    "\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _"
    1.70 +    "\<Lambda> (c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d"
    1.71  
    1.72    exE (Q): "\<lambda>x pq. pq x"
    1.73 -    "\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
    1.74 +    "\<Lambda> (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
    1.75  
    1.76    exE: "Null"
    1.77 -    "\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
    1.78 +    "\<Lambda> P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
    1.79  
    1.80    conjI (P, Q): "Pair"
    1.81 -    "\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h"
    1.82 +    "\<Lambda> (c: _) (d: _) P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> c \<bullet> d \<bullet> h"
    1.83  
    1.84    conjI (P): "\<lambda>p. p"
    1.85 -    "\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _"
    1.86 +    "\<Lambda> (c: _) P Q p. conjI \<cdot> _ \<cdot> _"
    1.87  
    1.88    conjI (Q): "\<lambda>q. q"
    1.89 -    "\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
    1.90 +    "\<Lambda> (c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
    1.91  
    1.92    conjI: "Null" "conjI"
    1.93  
    1.94    conjunct1 (P, Q): "fst"
    1.95 -    "\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _"
    1.96 +    "\<Lambda> (c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _"
    1.97  
    1.98    conjunct1 (P): "\<lambda>p. p"
    1.99 -    "\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _"
   1.100 +    "\<Lambda> (c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _"
   1.101  
   1.102    conjunct1 (Q): "Null"
   1.103 -    "\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _"
   1.104 +    "\<Lambda> (c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _"
   1.105  
   1.106    conjunct1: "Null" "conjunct1"
   1.107  
   1.108    conjunct2 (P, Q): "snd"
   1.109 -    "\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _"
   1.110 +    "\<Lambda> (c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _"
   1.111  
   1.112    conjunct2 (P): "Null"
   1.113 -    "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.114 +    "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.115  
   1.116    conjunct2 (Q): "\<lambda>p. p"
   1.117 -    "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.118 +    "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.119  
   1.120    conjunct2: "Null" "conjunct2"
   1.121  
   1.122    disjI1 (P, Q): "Inl"
   1.123 -    "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)"
   1.124 +    "\<Lambda> (c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
   1.125  
   1.126    disjI1 (P): "Some"
   1.127 -    "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)"
   1.128 +    "\<Lambda> (c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
   1.129  
   1.130    disjI1 (Q): "None"
   1.131 -    "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
   1.132 +    "\<Lambda> (c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
   1.133  
   1.134    disjI1: "Left"
   1.135 -    "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)"
   1.136 +    "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
   1.137  
   1.138    disjI2 (P, Q): "Inr"
   1.139 -    "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
   1.140 +    "\<Lambda> (d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
   1.141  
   1.142    disjI2 (P): "None"
   1.143 -    "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
   1.144 +    "\<Lambda> (c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
   1.145  
   1.146    disjI2 (Q): "Some"
   1.147 -    "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
   1.148 +    "\<Lambda> (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
   1.149  
   1.150    disjI2: "Right"
   1.151 -    "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)"
   1.152 +    "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
   1.153  
   1.154    disjE (P, Q, R): "\<lambda>pq pr qr.
   1.155       (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
   1.156 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
   1.157 -       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.158 +    "\<Lambda> (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr.
   1.159 +       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2"
   1.160  
   1.161    disjE (Q, R): "\<lambda>pq pr qr.
   1.162       (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
   1.163 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
   1.164 -       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.165 +    "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr.
   1.166 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2"
   1.167  
   1.168    disjE (P, R): "\<lambda>pq pr qr.
   1.169       (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
   1.170 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _).
   1.171 -       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.172 +    "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _).
   1.173 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.174  
   1.175    disjE (R): "\<lambda>pq pr qr.
   1.176       (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
   1.177 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
   1.178 -       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.179 +    "\<Lambda> (c: _) P Q R pq (h1: _) pr (h2: _) qr.
   1.180 +       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2"
   1.181  
   1.182    disjE (P, Q): "Null"
   1.183 -    "\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
   1.184 +    "\<Lambda> (c: _) (d: _) P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d \<bullet> arity_type_bool"
   1.185  
   1.186    disjE (Q): "Null"
   1.187 -    "\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
   1.188 +    "\<Lambda> (c: _) P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool"
   1.189  
   1.190    disjE (P): "Null"
   1.191 -    "\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _).
   1.192 -       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.193 +    "\<Lambda> (c: _) P Q R pq (h1: _) (h2: _) (h3: _).
   1.194 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.195  
   1.196    disjE: "Null"
   1.197 -    "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
   1.198 +    "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool"
   1.199  
   1.200    FalseE (P): "default"
   1.201 -    "\<Lambda> P. FalseE \<cdot> _"
   1.202 +    "\<Lambda> (c: _) P. FalseE \<cdot> _"
   1.203  
   1.204    FalseE: "Null" "FalseE"
   1.205  
   1.206    notI (P): "Null"
   1.207 -    "\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
   1.208 +    "\<Lambda> (c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
   1.209  
   1.210    notI: "Null" "notI"
   1.211  
   1.212    notE (P, R): "\<lambda>p. default"
   1.213 -    "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.214 +    "\<Lambda> (c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
   1.215  
   1.216    notE (P): "Null"
   1.217 -    "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.218 +    "\<Lambda> (c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
   1.219  
   1.220    notE (R): "default"
   1.221 -    "\<Lambda> P R. notE \<cdot> _ \<cdot> _"
   1.222 +    "\<Lambda> (c: _) P R. notE \<cdot> _ \<cdot> _"
   1.223  
   1.224    notE: "Null" "notE"
   1.225  
   1.226    subst (P): "\<lambda>s t ps. ps"
   1.227 -    "\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h"
   1.228 +    "\<Lambda> (c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h"
   1.229  
   1.230    subst: "Null" "subst"
   1.231  
   1.232    iffD1 (P, Q): "fst"
   1.233 -    "\<Lambda> Q P pq (h: _) p.
   1.234 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.235 +    "\<Lambda> (d: _) (c: _) Q P pq (h: _) p.
   1.236 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.237  
   1.238    iffD1 (P): "\<lambda>p. p"
   1.239 -    "\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.240 +    "\<Lambda> (c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.241  
   1.242    iffD1 (Q): "Null"
   1.243 -    "\<Lambda> Q P q1 (h: _) q2.
   1.244 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.245 +    "\<Lambda> (c: _) Q P q1 (h: _) q2.
   1.246 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.247  
   1.248    iffD1: "Null" "iffD1"
   1.249  
   1.250    iffD2 (P, Q): "snd"
   1.251 -    "\<Lambda> P Q pq (h: _) q.
   1.252 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.253 +    "\<Lambda> (c: _) (d: _) P Q pq (h: _) q.
   1.254 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.255  
   1.256    iffD2 (P): "\<lambda>p. p"
   1.257 -    "\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.258 +    "\<Lambda> (c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.259  
   1.260    iffD2 (Q): "Null"
   1.261 -    "\<Lambda> P Q q1 (h: _) q2.
   1.262 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.263 +    "\<Lambda> (c: _) P Q q1 (h: _) q2.
   1.264 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.265  
   1.266    iffD2: "Null" "iffD2"
   1.267  
   1.268    iffI (P, Q): "Pair"
   1.269 -    "\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
   1.270 +    "\<Lambda> (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
   1.271         (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot>
   1.272         (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet>
   1.273 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.274 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.275 +       (arity_type_fun \<bullet> c \<bullet> d) \<bullet>
   1.276 +       (arity_type_fun \<bullet> d \<bullet> c) \<bullet>
   1.277 +       (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.278 +       (allI \<cdot> _ \<bullet> d \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.279  
   1.280    iffI (P): "\<lambda>p. p"
   1.281 -    "\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.282 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.283 +    "\<Lambda> (c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.284 +       (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.285         (impI \<cdot> _ \<cdot> _ \<bullet> h2)"
   1.286  
   1.287    iffI (Q): "\<lambda>q. q"
   1.288 -    "\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.289 +    "\<Lambda> (c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.290         (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
   1.291 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.292 +       (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.293  
   1.294    iffI: "Null" "iffI"
   1.295  
   1.296 -(*
   1.297 -  classical: "Null"
   1.298 -    "\<Lambda> P. classical \<cdot> _"
   1.299 -*)
   1.300 -
   1.301 -setup {*
   1.302 -  Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"})
   1.303 -*}
   1.304 -
   1.305  end
     2.1 --- a/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:18:51 2010 +0200
     2.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:30:57 2010 +0200
     2.3 @@ -264,6 +264,7 @@
     2.4  lemmas [extraction_expand] = conj_assoc listall_cons_eq
     2.5  
     2.6  extract type_NF
     2.7 +
     2.8  lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
     2.9    apply (rule iffI)
    2.10    apply (erule rtranclpR.induct)
     3.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 01 11:18:51 2010 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 01 11:30:57 2010 +0200
     3.3 @@ -22,10 +22,6 @@
     3.4      in map (fn ks => i::ks) is @ is end
     3.5    else [[]];
     3.6  
     3.7 -fun forall_intr_prf (t, prf) =
     3.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     3.9 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    3.10 -
    3.11  fun prf_of thm =
    3.12    Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    3.13  
    3.14 @@ -130,12 +126,12 @@
    3.15  
    3.16      val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
    3.17      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    3.18 -    val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
    3.19 -      member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
    3.20 +    val ivs1 = map Var (filter_out (fn (_, T) =>
    3.21 +      @{type_name bool} = tname_of (body_type T)) ivs);
    3.22      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    3.23  
    3.24      val prf =
    3.25 -      List.foldr forall_intr_prf
    3.26 +      Extraction.abs_corr_shyps thy' induct vs ivs2
    3.27          (fold_rev (fn (f, p) => fn prf =>
    3.28            (case head_of (strip_abs_body f) of
    3.29               Free (s, T) =>
    3.30 @@ -145,7 +141,7 @@
    3.31                 end
    3.32            | _ => AbsP ("H", SOME p, prf)))
    3.33              (rec_fns ~~ prems_of thm)
    3.34 -            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
    3.35 +            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    3.36  
    3.37      val r' =
    3.38        if null is then r
    3.39 @@ -198,18 +194,21 @@
    3.40        ||> Sign.restore_naming thy;
    3.41  
    3.42      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    3.43 -    val prf = forall_intr_prf (y, forall_intr_prf (P,
    3.44 -      fold_rev (fn (p, r) => fn prf =>
    3.45 -          forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
    3.46 +    val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
    3.47 +      (fold_rev (fn (p, r) => fn prf =>
    3.48 +          Proofterm.forall_intr_proof' (Logic.varify_global r)
    3.49 +            (AbsP ("H", SOME (Logic.varify_global p), prf)))
    3.50          (prems ~~ rs)
    3.51 -        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
    3.52 +        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    3.53 +    val prf' = Extraction.abs_corr_shyps thy' exhaust []
    3.54 +      (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
    3.55      val r' = Logic.varify_global (Abs ("y", T,
    3.56        list_abs (map dest_Free rs, list_comb (r,
    3.57          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    3.58  
    3.59    in Extraction.add_realizers_i
    3.60      [(exh_name, (["P"], r', prf)),
    3.61 -     (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
    3.62 +     (exh_name, ([], Extraction.nullt, prf'))] thy'
    3.63    end;
    3.64  
    3.65  fun add_dt_realizers config names thy =
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:18:51 2010 +0200
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:30:57 2010 +0200
     4.3 @@ -21,18 +21,12 @@
     4.4      [name] => name
     4.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
     4.6  
     4.7 -val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
     4.8 -
     4.9  fun prf_of thm =
    4.10    let
    4.11      val thy = Thm.theory_of_thm thm;
    4.12      val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    4.13    in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    4.14  
    4.15 -fun forall_intr_prf t prf =
    4.16 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    4.17 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    4.18 -
    4.19  fun subsets [] = [[]]
    4.20    | subsets (x::xs) =
    4.21        let val ys = subsets xs
    4.22 @@ -55,15 +49,19 @@
    4.23        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    4.24    | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
    4.25  
    4.26 -fun relevant_vars prop = List.foldr (fn
    4.27 -      (Var ((a, i), T), vs) => (case strip_type T of
    4.28 +fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
    4.29 +     (case strip_type T of
    4.30          (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
    4.31 -      | _ => vs)
    4.32 -    | (_, vs) => vs) [] (OldTerm.term_vars prop);
    4.33 +      | _ => vs)) (Term.add_vars prop []) [];
    4.34 +
    4.35 +val attach_typeS = map_types (map_atyps
    4.36 +  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
    4.37 +    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
    4.38 +    | T => T));
    4.39  
    4.40  fun dt_of_intrs thy vs nparms intrs =
    4.41    let
    4.42 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    4.43 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
    4.44      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    4.45        (Logic.strip_imp_concl (prop_of (hd intrs))));
    4.46      val params = map dest_Var (take nparms ts);
    4.47 @@ -84,7 +82,7 @@
    4.48  fun gen_rvar vs (t as Var ((a, 0), T)) =
    4.49        if body_type T <> HOLogic.boolT then t else
    4.50          let
    4.51 -          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
    4.52 +          val U = TVar (("'" ^ a, 0), [])
    4.53            val Ts = binder_types T;
    4.54            val i = length Ts;
    4.55            val xs = map (pair "x") Ts;
    4.56 @@ -98,8 +96,9 @@
    4.57  
    4.58  fun mk_realizes_eqn n vs nparms intrs =
    4.59    let
    4.60 -    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
    4.61 -    val iTs = OldTerm.term_tvars concl;
    4.62 +    val intr = map_types Type.strip_sorts (prop_of (hd intrs));
    4.63 +    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
    4.64 +    val iTs = rev (Term.add_tvars intr []);
    4.65      val Tvs = map TVar iTs;
    4.66      val (h as Const (s, T), us) = strip_comb concl;
    4.67      val params = List.take (us, nparms);
    4.68 @@ -110,7 +109,7 @@
    4.69        (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
    4.70      val rT = if n then Extraction.nullT
    4.71        else Type (space_implode "_" (s ^ "T" :: vs),
    4.72 -        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
    4.73 +        map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
    4.74      val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
    4.75      val S = list_comb (h, params @ xs);
    4.76      val rvs = relevant_vars S;
    4.77 @@ -121,7 +120,7 @@
    4.78        let val T = (the o AList.lookup (op =) rvs) v
    4.79        in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
    4.80          Extraction.mk_typ (if n then Extraction.nullT
    4.81 -          else TVar (("'" ^ v, 0), HOLogic.typeS)))
    4.82 +          else TVar (("'" ^ v, 0), [])))
    4.83        end;
    4.84  
    4.85      val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
    4.86 @@ -261,12 +260,12 @@
    4.87      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    4.88      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
    4.89      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
    4.90 -    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
    4.91 -    val rlz'' = fold_rev Logic.all vs2 rlz
    4.92 +    val rlz' = fold_rev Logic.all rs (prop_of rrule)
    4.93    in (name, (vs,
    4.94      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    4.95 -    ProofRewriteRules.un_hhf_proof rlz' rlz''
    4.96 -      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
    4.97 +    Extraction.abs_corr_shyps thy rule vs vs2
    4.98 +      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
    4.99 +         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
   4.100    end;
   4.101  
   4.102  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
   4.103 @@ -275,7 +274,7 @@
   4.104    let
   4.105      val qualifier = Long_Name.qualifier (name_of_thm induct);
   4.106      val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
   4.107 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
   4.108 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
   4.109      val ar = length vs + length iTs;
   4.110      val params = Inductive.params_of raw_induct;
   4.111      val arities = Inductive.arities_of raw_induct;
   4.112 @@ -297,8 +296,6 @@
   4.113      val thy1' = thy1 |>
   4.114        Theory.copy |>
   4.115        Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
   4.116 -      fold (fn s => AxClass.axiomatize_arity
   4.117 -        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   4.118          Extraction.add_typeof_eqns_i ty_eqs;
   4.119      val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
   4.120        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   4.121 @@ -328,10 +325,10 @@
   4.122          end
   4.123        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
   4.124          rss (rec_thms, dummies);
   4.125 -    val rintrs = map (fn (intr, c) => Envir.eta_contract
   4.126 +    val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
   4.127        (Extraction.realizes_of thy2 vs
   4.128          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   4.129 -          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
   4.130 +          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
   4.131              (maps snd rss ~~ flat constrss);
   4.132      val (rlzpreds, rlzpreds') =
   4.133        rintrs |> map (fn rintr =>
   4.134 @@ -390,7 +387,9 @@
   4.135          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   4.136            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
   4.137          val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
   4.138 -        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
   4.139 +        val thm = Goal.prove_global thy []
   4.140 +          (map attach_typeS prems) (attach_typeS concl)
   4.141 +          (fn {prems, ...} => EVERY
   4.142            [rtac (#raw_induct ind_info) 1,
   4.143             rewrite_goals_tac rews,
   4.144             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   4.145 @@ -408,10 +407,10 @@
   4.146        in
   4.147          Extraction.add_realizers_i
   4.148            (map (fn (((ind, corr), rlz), r) =>
   4.149 -              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
   4.150 +              mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
   4.151              realizers @ (case realizers of
   4.152               [(((ind, corr), rlz), r)] =>
   4.153 -               [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   4.154 +               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   4.155                    ind, corr, rlz, r)]
   4.156             | _ => [])) thy''
   4.157        end;
   4.158 @@ -445,7 +444,7 @@
   4.159              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   4.160              [Bound (length prems)]));
   4.161          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   4.162 -        val rlz' = strip_all (Logic.unvarify_global rlz);
   4.163 +        val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
   4.164          val rews = map mk_meta_eq case_thms;
   4.165          val thm = Goal.prove_global thy []
   4.166            (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
   4.167 @@ -488,7 +487,7 @@
   4.168      val vss = sort (int_ord o pairself length)
   4.169        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   4.170    in
   4.171 -    fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   4.172 +    fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   4.173    end
   4.174  
   4.175  fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
     5.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 01 11:18:51 2010 +0200
     5.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 01 11:30:57 2010 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  signature REWRITE_HOL_PROOF =
     5.5  sig
     5.6    val rews: (Proofterm.proof * Proofterm.proof) list
     5.7 -  val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     5.8 +  val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     5.9  end;
    5.10  
    5.11  structure RewriteHOLProof : REWRITE_HOL_PROOF =
    5.12 @@ -16,7 +16,7 @@
    5.13  open Proofterm;
    5.14  
    5.15  val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
    5.16 -    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
    5.17 +    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
    5.18  
    5.19    (** eliminate meta-equality rules **)
    5.20  
    5.21 @@ -24,237 +24,258 @@
    5.22   \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
    5.23   \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
    5.24   \  (iffD1 % A % B %%  \
    5.25 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
    5.26 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    5.27  
    5.28     "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
    5.29   \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
    5.30   \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
    5.31   \  (iffD2 % A % B %%  \
    5.32 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
    5.33 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    5.34  
    5.35 -   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
    5.36 +   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %%  \
    5.37   \    (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==  \
    5.38   \  (cong % TYPE('T) % TYPE('U) % f % g % x % y %%  \
    5.39 - \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
    5.40 - \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
    5.41 -
    5.42 -   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
    5.43 - \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    5.44 - \  (HOL.trans % TYPE('T) % x % y % z %%  \
    5.45 - \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
    5.46 - \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
    5.47 + \    (OfClass type_class % TYPE('T)) %% prfU %%  \
    5.48 + \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %%  \
    5.49 + \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
    5.50  
    5.51 -   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
    5.52 - \  (HOL.refl % TYPE('T) % x)",
    5.53 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %%  \
    5.54 + \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    5.55 + \  (HOL.trans % TYPE('T) % x % y % z %% prfT %%  \
    5.56 + \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %%  \
    5.57 + \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
    5.58  
    5.59 -   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    5.60 +   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) ==  \
    5.61 + \  (HOL.refl % TYPE('T) % x %% prfT)",
    5.62 +
    5.63 +   "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    5.64   \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
    5.65 - \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
    5.66 + \  (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
    5.67  
    5.68 -   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
    5.69 +   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %%  \
    5.70   \    (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==  \
    5.71   \  (ext % TYPE('T) % TYPE('U) % f % g %%  \
    5.72 - \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
    5.73 + \    (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %%  \
    5.74 + \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %%  \
    5.75 + \       (OfClass type_class % TYPE('U)) %% (prf % x)))",
    5.76  
    5.77 -   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    5.78 - \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
    5.79 +   "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    5.80 + \    (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
    5.81  
    5.82 -   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    5.83 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
    5.84   \    (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    5.85   \      (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    5.86   \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
    5.87   \  (iffD1 % A = C % B = D %%  \
    5.88 - \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
    5.89 + \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
    5.90 + \      prfT %% arity_type_bool %%  \
    5.91   \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    5.92   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    5.93 - \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    5.94 - \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    5.95 - \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    5.96 - \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
    5.97 + \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
    5.98 + \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
    5.99 + \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
   5.100 + \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
   5.101 + \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
   5.102 + \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
   5.103  
   5.104 -   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
   5.105 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
   5.106   \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
   5.107   \      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
   5.108   \        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
   5.109   \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
   5.110   \  (iffD2 % A = C % B = D %%  \
   5.111 - \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
   5.112 + \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
   5.113 + \      prfT %% arity_type_bool %%  \
   5.114   \      (cong % TYPE('T) % TYPE('T=>bool) %  \
   5.115   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
   5.116 - \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
   5.117 - \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
   5.118 - \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
   5.119 - \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
   5.120 + \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
   5.121 + \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
   5.122 + \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
   5.123 + \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
   5.124 + \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
   5.125 + \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
   5.126  
   5.127     (** rewriting on bool: insert proper congruence rules for logical connectives **)
   5.128  
   5.129     (* All *)
   5.130  
   5.131 -   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
   5.132 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   5.133 - \  (allI % TYPE('a) % Q %%  \
   5.134 +   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   5.135 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   5.136 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   5.137 + \  (allI % TYPE('a) % Q %% prfa %%  \
   5.138   \    (Lam x.  \
   5.139   \        iffD1 % P x % Q x %% (prf % x) %%  \
   5.140 - \         (spec % TYPE('a) % P % x %% prf')))",
   5.141 + \         (spec % TYPE('a) % P % x %% prfa %% prf')))",
   5.142  
   5.143 -   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
   5.144 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   5.145 - \  (allI % TYPE('a) % P %%  \
   5.146 +   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   5.147 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   5.148 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   5.149 + \  (allI % TYPE('a) % P %% prfa %%  \
   5.150   \    (Lam x.  \
   5.151   \        iffD2 % P x % Q x %% (prf % x) %%  \
   5.152 - \         (spec % TYPE('a) % Q % x %% prf')))",
   5.153 + \         (spec % TYPE('a) % Q % x %% prfa %% prf')))",
   5.154  
   5.155     (* Ex *)
   5.156  
   5.157 -   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
   5.158 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   5.159 - \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
   5.160 +   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   5.161 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   5.162 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   5.163 + \  (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %%  \
   5.164   \    (Lam x H : P x.  \
   5.165 - \        exI % TYPE('a) % Q % x %%  \
   5.166 + \        exI % TYPE('a) % Q % x %% prfa %%  \
   5.167   \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
   5.168  
   5.169 -   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
   5.170 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   5.171 - \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
   5.172 +   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   5.173 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   5.174 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   5.175 + \  (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %%  \
   5.176   \    (Lam x H : Q x.  \
   5.177 - \        exI % TYPE('a) % P % x %%  \
   5.178 + \        exI % TYPE('a) % P % x %% prfa %%  \
   5.179   \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
   5.180  
   5.181     (* & *)
   5.182  
   5.183 -   "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   5.184 - \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
   5.185 - \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
   5.186 +   "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   5.187 + \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %%  \
   5.188 + \      (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   5.189   \  (conjI % B % D %%  \
   5.190   \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
   5.191   \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
   5.192  
   5.193 -   "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   5.194 - \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
   5.195 - \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
   5.196 +   "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   5.197 + \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %%  \
   5.198 + \      (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   5.199   \  (conjI % A % C %%  \
   5.200   \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
   5.201   \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
   5.202  
   5.203 -   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
   5.204 - \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
   5.205 - \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
   5.206 +   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %%  \
   5.207 + \    (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) ==  \
   5.208 + \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %%  \
   5.209   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   5.210   \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
   5.211 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
   5.212 - \        (HOL.refl % TYPE(bool) % A)))",
   5.213 + \        prfb %% prfbb %%  \
   5.214 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %%  \
   5.215 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   5.216 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   5.217  
   5.218     (* | *)
   5.219  
   5.220 -   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   5.221 - \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   5.222 - \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   5.223 +   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   5.224 + \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %%  \
   5.225 + \      (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   5.226   \  (disjE % A % C % B | D %% prf3 %%  \
   5.227   \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
   5.228   \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
   5.229  
   5.230 -   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   5.231 - \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   5.232 - \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   5.233 +   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   5.234 + \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %%  \
   5.235 + \      (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   5.236   \  (disjE % B % D % A | C %% prf3 %%  \
   5.237   \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
   5.238   \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
   5.239  
   5.240 -   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   5.241 - \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
   5.242 - \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   5.243 +   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %%  \
   5.244 + \    (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) ==  \
   5.245 + \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %%  \
   5.246   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   5.247   \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
   5.248 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
   5.249 - \        (HOL.refl % TYPE(bool) % A)))",
   5.250 + \        prfb %% prfbb %%  \
   5.251 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %%  \
   5.252 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   5.253 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   5.254  
   5.255     (* --> *)
   5.256  
   5.257 -   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   5.258 - \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   5.259 - \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   5.260 +   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   5.261 + \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %%  \
   5.262 + \      (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   5.263   \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
   5.264   \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
   5.265  
   5.266 -   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   5.267 - \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   5.268 - \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   5.269 +   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   5.270 + \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %%  \
   5.271 + \      (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   5.272   \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
   5.273   \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
   5.274  
   5.275 -   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   5.276 - \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
   5.277 - \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   5.278 +   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %%  \
   5.279 + \    (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) ==  \
   5.280 + \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %%  \
   5.281   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   5.282   \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
   5.283 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
   5.284 - \        (HOL.refl % TYPE(bool) % A)))",
   5.285 + \        prfb %% prfbb %%  \
   5.286 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %%  \
   5.287 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   5.288 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   5.289  
   5.290     (* ~ *)
   5.291  
   5.292 -   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   5.293 - \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   5.294 +   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   5.295 + \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   5.296   \  (notI % Q %% (Lam H: Q.  \
   5.297   \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
   5.298  
   5.299 -   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   5.300 - \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   5.301 +   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   5.302 + \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   5.303   \  (notI % P %% (Lam H: P.  \
   5.304   \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
   5.305  
   5.306     (* = *)
   5.307  
   5.308     "(iffD1 % B % D %%  \
   5.309 - \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   5.310 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   5.311 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   5.312 + \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   5.313 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   5.314 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   5.315   \  (iffD1 % C % D %% prf2 %%  \
   5.316   \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   5.317  
   5.318     "(iffD2 % B % D %%  \
   5.319 - \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   5.320 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   5.321 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   5.322 + \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   5.323 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   5.324 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   5.325   \  (iffD1 % A % B %% prf1 %%  \
   5.326   \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   5.327  
   5.328     "(iffD1 % A % C %%  \
   5.329 - \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   5.330 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   5.331 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   5.332 + \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   5.333 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   5.334 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   5.335   \  (iffD2 % C % D %% prf2 %%  \
   5.336   \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   5.337  
   5.338     "(iffD2 % A % C %%  \
   5.339 - \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   5.340 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   5.341 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   5.342 + \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   5.343 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   5.344 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   5.345   \  (iffD2 % A % B %% prf1 %%  \
   5.346   \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   5.347  
   5.348 -   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   5.349 - \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
   5.350 - \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   5.351 +   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   5.352 + \    (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) ==  \
   5.353 + \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   5.354   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   5.355   \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   5.356 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
   5.357 - \        (HOL.refl % TYPE(bool) % A)))",
   5.358 + \        prfb %% prfbb %%  \
   5.359 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %%  \
   5.360 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   5.361 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   5.362  
   5.363     (** transitivity, reflexivity, and symmetry **)
   5.364  
   5.365 -   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   5.366 +   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   5.367   \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
   5.368  
   5.369 -   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   5.370 +   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   5.371   \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
   5.372  
   5.373 -   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
   5.374 +   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   5.375  
   5.376 -   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
   5.377 +   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   5.378  
   5.379 -   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
   5.380 +   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
   5.381  
   5.382 -   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
   5.383 +   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
   5.384  
   5.385     (** normalization of HOL proofs **)
   5.386  
   5.387 @@ -262,13 +283,13 @@
   5.388  
   5.389     "(impI % A % B %% (mp % A % B %% prf)) == prf",
   5.390  
   5.391 -   "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
   5.392 +   "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
   5.393  
   5.394 -   "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
   5.395 +   "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
   5.396  
   5.397 -   "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
   5.398 +   "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
   5.399  
   5.400 -   "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
   5.401 +   "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
   5.402  
   5.403     "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
   5.404  
   5.405 @@ -286,26 +307,26 @@
   5.406  (** Replace congruence rules by substitution rules **)
   5.407  
   5.408  fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
   5.409 -      prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
   5.410 -  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
   5.411 +      prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
   5.412 +  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
   5.413    | strip_cong _ _ = NONE;
   5.414  
   5.415 -val subst_prf = fst (strip_combt (Thm.proof_of subst));
   5.416 -val sym_prf = fst (strip_combt (Thm.proof_of sym));
   5.417 +val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
   5.418 +val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
   5.419  
   5.420  fun make_subst Ts prf xs (_, []) = prf
   5.421 -  | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
   5.422 +  | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
   5.423        let val T = fastype_of1 (Ts, x)
   5.424        in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
   5.425          else change_type (SOME [T]) subst_prf %> x %> y %>
   5.426            Abs ("z", T, list_comb (incr_boundvars 1 f,
   5.427              map (incr_boundvars 1) xs @ Bound 0 ::
   5.428 -            map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
   5.429 +            map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
   5.430            make_subst Ts prf (xs @ [x]) (f, ps)
   5.431        end;
   5.432  
   5.433 -fun make_sym Ts ((x, y), prf) =
   5.434 -  ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
   5.435 +fun make_sym Ts ((x, y), (prf, clprf)) =
   5.436 +  ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
   5.437  
   5.438  fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
   5.439  
   5.440 @@ -322,6 +343,6 @@
   5.441          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
   5.442    | elim_cong_aux _ _ = NONE;
   5.443  
   5.444 -fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
   5.445 +fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
   5.446  
   5.447  end;
     6.1 --- a/src/Pure/Isar/class_target.ML	Tue Jun 01 11:18:51 2010 +0200
     6.2 +++ b/src/Pure/Isar/class_target.ML	Tue Jun 01 11:30:57 2010 +0200
     6.3 @@ -243,7 +243,7 @@
     6.4        | NONE => I
     6.5    in
     6.6      thy
     6.7 -    |> AxClass.add_classrel classrel
     6.8 +    |> AxClass.add_classrel true classrel
     6.9      |> ClassData.map (Graph.add_edge (sub, sup))
    6.10      |> activate_defs sub (these_defs thy diff_sort)
    6.11      |> add_dependency
    6.12 @@ -366,7 +366,7 @@
    6.13  fun gen_classrel mk_prop classrel thy =
    6.14    let
    6.15      fun after_qed results =
    6.16 -      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
    6.17 +      ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results);
    6.18    in
    6.19      thy
    6.20      |> ProofContext.init_global
    6.21 @@ -531,7 +531,7 @@
    6.22      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    6.23      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
    6.24      fun after_qed' results =
    6.25 -      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
    6.26 +      Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results)
    6.27        #> after_qed;
    6.28    in
    6.29      lthy
    6.30 @@ -591,7 +591,7 @@
    6.31      val sorts = map snd vs;
    6.32      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    6.33      fun after_qed results = ProofContext.theory
    6.34 -      ((fold o fold) AxClass.add_arity results);
    6.35 +      ((fold o fold) (AxClass.add_arity true) results);
    6.36    in
    6.37      thy
    6.38      |> ProofContext.init_global
     7.1 --- a/src/Pure/Proof/extraction.ML	Tue Jun 01 11:18:51 2010 +0200
     7.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jun 01 11:30:57 2010 +0200
     7.3 @@ -24,6 +24,7 @@
     7.4    val mk_typ : typ -> term
     7.5    val etype_of : theory -> string list -> typ list -> term -> typ
     7.6    val realizes_of: theory -> string list -> term -> term -> term
     7.7 +  val abs_corr_shyps: theory -> thm -> string list -> term list -> Proofterm.proof -> Proofterm.proof
     7.8  end;
     7.9  
    7.10  structure Extraction : EXTRACTION =
    7.11 @@ -126,11 +127,9 @@
    7.12  fun frees_of t = map Free (rev (Term.add_frees t []));
    7.13  fun vfs_of t = vars_of t @ frees_of t;
    7.14  
    7.15 -fun forall_intr_prf (t, prf) =
    7.16 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    7.17 -  in Abst (a, SOME T, prf_abstract_over t prf) end;
    7.18 +val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
    7.19  
    7.20 -val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    7.21 +val mkabsp = fold_rev (fn t => fn prf => AbsP ("H", SOME t, prf));
    7.22  
    7.23  fun strip_abs 0 t = t
    7.24    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
    7.25 @@ -161,6 +160,14 @@
    7.26      | _ => error "get_var_type: not a variable"
    7.27    end;
    7.28  
    7.29 +fun read_term thy T s =
    7.30 +  let
    7.31 +    val ctxt = ProofContext.init_global thy
    7.32 +      |> Proof_Syntax.strip_sorts_consttypes
    7.33 +      |> ProofContext.set_defsort [];
    7.34 +    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    7.35 +  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
    7.36 +
    7.37  
    7.38  (**** theory data ****)
    7.39  
    7.40 @@ -175,7 +182,7 @@
    7.41         (term -> typ -> term -> typ -> term) option)) list,
    7.42       realizers : (string list * (term * proof)) list Symtab.table,
    7.43       defs : thm list,
    7.44 -     expand : (string * term) list,
    7.45 +     expand : string list,
    7.46       prep : (theory -> proof -> proof) option}
    7.47  
    7.48    val empty =
    7.49 @@ -198,14 +205,14 @@
    7.50       types = AList.merge (op =) (K true) (types1, types2),
    7.51       realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
    7.52       defs = Library.merge Thm.eq_thm (defs1, defs2),
    7.53 -     expand = Library.merge (op =) (expand1, expand2),   (* FIXME proper aconv !?! *)
    7.54 +     expand = Library.merge (op =) (expand1, expand2),
    7.55       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    7.56  );
    7.57  
    7.58  fun read_condeq thy =
    7.59    let val thy' = add_syntax thy
    7.60    in fn s =>
    7.61 -    let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
    7.62 +    let val t = Logic.varify_global (read_term thy' propT s)
    7.63      in
    7.64        (map Logic.dest_equals (Logic.strip_imp_prems t),
    7.65          Logic.dest_equals (Logic.strip_imp_concl t))
    7.66 @@ -274,7 +281,7 @@
    7.67      fun err () = error ("Unable to determine type of extracted program for\n" ^
    7.68        Syntax.string_of_term_global thy t)
    7.69    in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
    7.70 -    [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
    7.71 +    [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
    7.72        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
    7.73        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
    7.74      | _ => err ()
    7.75 @@ -300,25 +307,30 @@
    7.76      val rtypes = map fst types;
    7.77      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    7.78      val thy' = add_syntax thy;
    7.79 -    val rd = Proof_Syntax.read_proof thy' false;
    7.80 +    val rd = Proof_Syntax.read_proof thy' true false;
    7.81    in fn (thm, (vs, s1, s2)) =>
    7.82      let
    7.83        val name = Thm.derivation_name thm;
    7.84        val _ = name <> "" orelse error "add_realizers: unnamed theorem";
    7.85 -      val prop = Pattern.rewrite_term thy'
    7.86 -        (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    7.87 +      val prop = Thm.unconstrainT thm |> prop_of |>
    7.88 +        Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [];
    7.89        val vars = vars_of prop;
    7.90        val vars' = filter_out (fn v =>
    7.91          member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
    7.92 +      val shyps = maps (fn Var ((x, i), _) =>
    7.93 +        if member (op =) vs x then Logic.mk_of_sort
    7.94 +          (TVar (("'" ^ x, i), []), Sign.defaultS thy')
    7.95 +        else []) vars;
    7.96        val T = etype_of thy' vs [] prop;
    7.97        val (T', thw) = Type.legacy_freeze_thaw_type
    7.98          (if T = nullT then nullT else map fastype_of vars' ---> T);
    7.99 -      val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
   7.100 +      val t = map_types thw (read_term thy' T' s1);
   7.101        val r' = freeze_thaw (condrew thy' eqns
   7.102 -        (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   7.103 +        (procs @ [typeof_proc [] vs, rlz_proc]))
   7.104            (Const ("realizes", T --> propT --> propT) $
   7.105              (if T = nullT then t else list_comb (t, vars')) $ prop);
   7.106 -      val r = fold_rev Logic.all (map (get_var_type r') vars) r';
   7.107 +      val r = Logic.list_implies (shyps,
   7.108 +        fold_rev Logic.all (map (get_var_type r') vars) r');
   7.109        val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
   7.110      in (name, (vs, (t, prf))) end
   7.111    end;
   7.112 @@ -337,10 +349,34 @@
   7.113      val prop' = Pattern.rewrite_term thy'
   7.114        (map (Logic.dest_equals o prop_of) defs) [] prop;
   7.115    in freeze_thaw (condrew thy' eqns
   7.116 -    (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   7.117 +    (procs @ [typeof_proc [] vs, rlz_proc]))
   7.118        (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
   7.119    end;
   7.120  
   7.121 +fun abs_corr_shyps thy thm vs xs prf =
   7.122 +  let
   7.123 +    val S = Sign.defaultS thy;
   7.124 +    val ((atyp_map, constraints, _), prop') =
   7.125 +      Logic.unconstrainT (#shyps (rep_thm thm)) (prop_of thm);
   7.126 +    val atyps = fold_types (fold_atyps (insert (op =))) (prop_of thm) [];
   7.127 +    val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
   7.128 +        SOME (TVar (("'" ^ v, i), [])) else NONE)
   7.129 +      (rev (Term.add_vars prop' []));
   7.130 +    val cs = maps (fn T => map (pair T) S) Ts;
   7.131 +    val constraints' = map Logic.mk_of_class cs;
   7.132 +    val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
   7.133 +    fun typ_map T = Type.strip_sorts
   7.134 +      (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
   7.135 +    fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
   7.136 +    val xs' = map (map_types typ_map) xs
   7.137 +  in
   7.138 +    prf |>
   7.139 +    Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
   7.140 +    fold_rev implies_intr_proof' (map snd constraints) |>
   7.141 +    fold_rev forall_intr_proof' xs' |>
   7.142 +    fold_rev implies_intr_proof' constraints'
   7.143 +  end;
   7.144 +
   7.145  (** expanding theorems / definitions **)
   7.146  
   7.147  fun add_expand_thm is_def thm thy =
   7.148 @@ -354,15 +390,15 @@
   7.149      thy |> ExtractionData.put
   7.150        (if is_def then
   7.151          {realizes_eqns = realizes_eqns,
   7.152 -         typeof_eqns = add_rule ([],
   7.153 -           Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
   7.154 +         typeof_eqns = add_rule ([], Logic.dest_equals (map_types
   7.155 +           Type.strip_sorts (prop_of (Drule.abs_def thm)))) typeof_eqns,
   7.156           types = types,
   7.157           realizers = realizers, defs = insert Thm.eq_thm thm defs,
   7.158           expand = expand, prep = prep}
   7.159        else
   7.160          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
   7.161           realizers = realizers, defs = defs,
   7.162 -         expand = insert (op =) (name, prop_of thm) expand, prep = prep})
   7.163 +         expand = insert (op =) name expand, prep = prep})
   7.164    end;
   7.165  
   7.166  fun extraction_expand is_def =
   7.167 @@ -443,9 +479,9 @@
   7.168        ExtractionData.get thy;
   7.169      val procs = maps (rev o fst o snd) types;
   7.170      val rtypes = map fst types;
   7.171 -    val typroc = typeof_proc (Sign.defaultS thy');
   7.172 +    val typroc = typeof_proc [];
   7.173      val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
   7.174 -      Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
   7.175 +      Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
   7.176      val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
   7.177  
   7.178      fun find_inst prop Ts ts vs =
   7.179 @@ -464,6 +500,13 @@
   7.180  
   7.181        in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
   7.182  
   7.183 +    fun mk_shyps tye = maps (fn (ixn, _) =>
   7.184 +      Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
   7.185 +
   7.186 +    fun mk_sprfs cs tye = maps (fn (_, T) =>
   7.187 +      ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
   7.188 +        (T, Sign.defaultS thy)) tye;
   7.189 +
   7.190      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
   7.191      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
   7.192  
   7.193 @@ -474,22 +517,22 @@
   7.194      fun realizes_null vs prop = app_rlz_rews [] vs
   7.195        (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
   7.196  
   7.197 -    fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i)
   7.198 +    fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
   7.199  
   7.200 -      | corr d defs vs ts Ts hs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
   7.201 +      | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
   7.202            let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
   7.203 -            (dummyt :: hs) prf (incr_pboundvars 1 0 prf')
   7.204 +            (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
   7.205              (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
   7.206            in (defs', Abst (s, SOME T, corr_prf)) end
   7.207  
   7.208 -      | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
   7.209 +      | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
   7.210            let
   7.211              val T = etype_of thy' vs Ts prop;
   7.212              val u = if T = nullT then 
   7.213                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
   7.214                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
   7.215              val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
   7.216 -              (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
   7.217 +              (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
   7.218              val rlz = Const ("realizes", T --> propT --> propT)
   7.219            in (defs',
   7.220              if T = nullT then AbsP ("R",
   7.221 @@ -500,10 +543,10 @@
   7.222                  (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
   7.223            end
   7.224  
   7.225 -      | corr d defs vs ts Ts hs (prf % SOME t) (prf' % _) t' =
   7.226 +      | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
   7.227            let
   7.228              val (Us, T) = strip_type (fastype_of1 (Ts, t));
   7.229 -            val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
   7.230 +            val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
   7.231                (if member (op =) rtypes (tname_of T) then t'
   7.232                 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
   7.233              val u = if not (member (op =) rtypes (tname_of T)) then t else
   7.234 @@ -519,7 +562,7 @@
   7.235                in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
   7.236            in (defs', corr_prf % SOME u) end
   7.237  
   7.238 -      | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
   7.239 +      | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
   7.240            let
   7.241              val prop = Reconstruct.prop_of' hs prf2';
   7.242              val T = etype_of thy' vs Ts prop;
   7.243 @@ -529,17 +572,19 @@
   7.244                 | _ =>
   7.245                   let val (defs1, u) = extr d defs vs [] Ts hs prf2'
   7.246                   in (defs1, NONE, SOME u) end)
   7.247 -            val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs prf1 prf1' f;
   7.248 -            val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs prf2 prf2' u;
   7.249 +            val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
   7.250 +            val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
   7.251            in
   7.252              if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
   7.253                (defs3, corr_prf1 % u %% corr_prf2)
   7.254            end
   7.255  
   7.256 -      | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
   7.257 +      | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
   7.258            let
   7.259              val prf = join_proof body;
   7.260              val (vs', tye) = find_inst prop Ts ts vs;
   7.261 +            val shyps = mk_shyps tye;
   7.262 +            val sprfs = mk_sprfs cs tye;
   7.263              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
   7.264              val T = etype_of thy' vs' [] prop;
   7.265              val defs' = if T = nullT then defs
   7.266 @@ -555,28 +600,31 @@
   7.267                        (if null vs' then ""
   7.268                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   7.269                      val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   7.270 -                    val (defs'', corr_prf) =
   7.271 -                      corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
   7.272 +                    val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
   7.273 +                      (rev shyps) prf' prf' NONE;
   7.274 +                    val corr_prf = mkabsp shyps corr_prf0;
   7.275                      val corr_prop = Reconstruct.prop_of corr_prf;
   7.276 -                    val corr_prf' = List.foldr forall_intr_prf
   7.277 -                      (proof_combt
   7.278 +                    val corr_prf' =
   7.279 +                      proof_combP (proof_combt
   7.280                           (PThm (serial (),
   7.281                            ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
   7.282 -                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
   7.283 -                      (map (get_var_type corr_prop) (vfs_of prop))
   7.284 +                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
   7.285 +                              map PBound (length shyps - 1 downto 0)) |>
   7.286 +                      fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
   7.287 +                      mkabsp shyps
   7.288                    in
   7.289                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
   7.290 -                     prf_subst_TVars tye' corr_prf')
   7.291 +                     proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
   7.292                    end
   7.293 -              | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf'))
   7.294 +              | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
   7.295              | SOME rs => (case find vs' rs of
   7.296 -                SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
   7.297 +                SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
   7.298                | NONE => error ("corr: no realizer for instance of theorem " ^
   7.299                    quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   7.300                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   7.301            end
   7.302  
   7.303 -      | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   7.304 +      | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   7.305            let
   7.306              val (vs', tye) = find_inst prop Ts ts vs;
   7.307              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   7.308 @@ -584,13 +632,14 @@
   7.309              if etype_of thy' vs' [] prop = nullT andalso
   7.310                realizes_null vs' prop aconv prop then (defs, prf0)
   7.311              else case find vs' (Symtab.lookup_list realizers s) of
   7.312 -              SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
   7.313 +              SOME (_, prf) => (defs,
   7.314 +                proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
   7.315              | NONE => error ("corr: no realizer for instance of axiom " ^
   7.316                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   7.317                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   7.318            end
   7.319  
   7.320 -      | corr d defs vs ts Ts hs _ _ _ = error "corr: bad proof"
   7.321 +      | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
   7.322  
   7.323      and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
   7.324  
   7.325 @@ -630,6 +679,7 @@
   7.326            let
   7.327              val prf = join_proof body;
   7.328              val (vs', tye) = find_inst prop Ts ts vs;
   7.329 +            val shyps = mk_shyps tye;
   7.330              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   7.331            in
   7.332              case Symtab.lookup realizers s of
   7.333 @@ -641,18 +691,18 @@
   7.334                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   7.335                      val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   7.336                      val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
   7.337 -                    val (defs'', corr_prf) =
   7.338 -                      corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
   7.339 +                    val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
   7.340 +                      (rev shyps) prf' prf' (SOME t);
   7.341  
   7.342                      val nt = Envir.beta_norm t;
   7.343                      val args = filter_out (fn v => member (op =) rtypes
   7.344                        (tname_of (body_type (fastype_of v)))) (vfs_of prop);
   7.345                      val args' = filter (fn v => Logic.occs (v, nt)) args;
   7.346 -                    val t' = mkabs nt args';
   7.347 +                    val t' = mkabs args' nt;
   7.348                      val T = fastype_of t';
   7.349                      val cname = extr_name s vs';
   7.350                      val c = Const (cname, T);
   7.351 -                    val u = mkabs (list_comb (c, args')) args;
   7.352 +                    val u = mkabs args (list_comb (c, args'));
   7.353                      val eqn = Logic.mk_equals (c, t');
   7.354                      val rlz =
   7.355                        Const ("realizes", fastype_of nt --> propT --> propT);
   7.356 @@ -661,20 +711,22 @@
   7.357                      val f = app_rlz_rews [] vs'
   7.358                        (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
   7.359  
   7.360 -                    val corr_prf' =
   7.361 -                      chtype [] equal_elim_axm %> lhs %> rhs %%
   7.362 +                    val corr_prf' = mkabsp shyps
   7.363 +                      (chtype [] equal_elim_axm %> lhs %> rhs %%
   7.364                         (chtype [propT] symmetric_axm %> rhs %> lhs %%
   7.365                           (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
   7.366                             (chtype [T --> propT] reflexive_axm %> f) %%
   7.367                             PAxm (cname ^ "_def", eqn,
   7.368 -                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
   7.369 +                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
   7.370                      val corr_prop = Reconstruct.prop_of corr_prf';
   7.371 -                    val corr_prf'' = List.foldr forall_intr_prf
   7.372 -                      (proof_combt
   7.373 +                    val corr_prf'' =
   7.374 +                      proof_combP (proof_combt
   7.375                          (PThm (serial (),
   7.376                           ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
   7.377 -                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
   7.378 -                      (map (get_var_type corr_prop) (vfs_of prop));
   7.379 +                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
   7.380 +                             map PBound (length shyps - 1 downto 0)) |>
   7.381 +                      fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
   7.382 +                      mkabsp shyps
   7.383                    in
   7.384                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
   7.385                       subst_TVars tye' u)
   7.386 @@ -731,7 +783,7 @@
   7.387             in
   7.388               thy'
   7.389               |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
   7.390 -                  Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
   7.391 +                  Thm.varifyT_global (funpow (length (vars_of corr_prop))
   7.392                      (Thm.forall_elim_var 0) (Thm.forall_intr_frees
   7.393                        (ProofChecker.thm_of_proof thy'
   7.394                         (fst (Proofterm.freeze_thaw_prf prf))))))
     8.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jun 01 11:18:51 2010 +0200
     8.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jun 01 11:30:57 2010 +0200
     8.3 @@ -6,14 +6,17 @@
     8.4  
     8.5  signature PROOF_REWRITE_RULES =
     8.6  sig
     8.7 -  val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     8.8 +  val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     8.9    val rprocs : bool ->
    8.10 -    (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
    8.11 +    (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
    8.12    val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    8.13    val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    8.14    val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
    8.15    val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    8.16    val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    8.17 +  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
    8.18 +  val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
    8.19 +    (Proofterm.proof * Proofterm.proof) option
    8.20  end;
    8.21  
    8.22  structure ProofRewriteRules : PROOF_REWRITE_RULES =
    8.23 @@ -21,7 +24,7 @@
    8.24  
    8.25  open Proofterm;
    8.26  
    8.27 -fun rew b _ =
    8.28 +fun rew b _ _ =
    8.29    let
    8.30      fun ?? x = if b then SOME x else NONE;
    8.31      fun ax (prf as PAxm (s, prop, _)) Ts =
    8.32 @@ -219,31 +222,36 @@
    8.33  fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
    8.34  
    8.35  fun insert_refl defs Ts (prf1 %% prf2) =
    8.36 -      insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
    8.37 +      let val (prf1', b) = insert_refl defs Ts prf1
    8.38 +      in
    8.39 +        if b then (prf1', true)
    8.40 +        else (prf1' %% fst (insert_refl defs Ts prf2), false)
    8.41 +      end
    8.42    | insert_refl defs Ts (Abst (s, SOME T, prf)) =
    8.43 -      Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
    8.44 +      (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
    8.45    | insert_refl defs Ts (AbsP (s, t, prf)) =
    8.46 -      AbsP (s, t, insert_refl defs Ts prf)
    8.47 +      (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
    8.48    | insert_refl defs Ts prf = (case strip_combt prf of
    8.49          (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
    8.50            if member (op =) defs s then
    8.51              let
    8.52                val vs = vars_of prop;
    8.53                val tvars = Term.add_tvars prop [] |> rev;
    8.54 -              val (_, rhs) = Logic.dest_equals prop;
    8.55 +              val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
    8.56                val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
    8.57                  (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
    8.58                  map the ts);
    8.59              in
    8.60 -              change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
    8.61 +              (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
    8.62              end
    8.63 -          else prf
    8.64 -      | (_, []) => prf
    8.65 -      | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
    8.66 +          else (prf, false)
    8.67 +      | (_, []) => (prf, false)
    8.68 +      | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
    8.69  
    8.70  fun elim_defs thy r defs prf =
    8.71    let
    8.72 -    val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
    8.73 +    val defs' = map (Logic.dest_equals o
    8.74 +      map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
    8.75      val defnames = map Thm.derivation_name defs;
    8.76      val f = if not r then I else
    8.77        let
    8.78 @@ -258,7 +266,7 @@
    8.79        in Reconstruct.expand_proof thy thms end;
    8.80    in
    8.81      rewrite_terms (Pattern.rewrite_term thy defs' [])
    8.82 -      (insert_refl defnames [] (f prf))
    8.83 +      (fst (insert_refl defnames [] (f prf)))
    8.84    end;
    8.85  
    8.86  
    8.87 @@ -327,4 +335,35 @@
    8.88      mk_prf Q
    8.89    end;
    8.90  
    8.91 +
    8.92 +(**** expand OfClass proofs ****)
    8.93 +
    8.94 +fun mk_of_sort_proof thy hs (T, S) =
    8.95 +  let
    8.96 +    val hs' = map
    8.97 +      (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
    8.98 +        | NONE => NONE) hs;
    8.99 +    val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
   8.100 +    fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
   8.101 +    val subst = map_atyps
   8.102 +      (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
   8.103 +        | T as TFree (s, _) => TFree (s, get_sort T));
   8.104 +    fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
   8.105 +        ~1 => error "expand_of_class: missing class hypothesis"
   8.106 +      | i => PBound i;
   8.107 +    fun reconstruct prf prop = prf |>
   8.108 +      Reconstruct.reconstruct_proof thy prop |>
   8.109 +      Reconstruct.expand_proof thy [("", NONE)] |>
   8.110 +      Same.commit (map_proof_same Same.same Same.same hyp)
   8.111 +  in
   8.112 +    map2 reconstruct
   8.113 +      (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
   8.114 +      (Logic.mk_of_sort (T, S))
   8.115 +  end;
   8.116 +
   8.117 +fun expand_of_class thy Ts hs (OfClass (T, c)) =
   8.118 +      mk_of_sort_proof thy hs (T, [c]) |>
   8.119 +      hd |> rpair no_skel |> SOME
   8.120 +  | expand_of_class thy Ts hs _ = NONE;
   8.121 +
   8.122  end;
     9.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 11:18:51 2010 +0200
     9.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 11:30:57 2010 +0200
     9.3 @@ -11,8 +11,9 @@
     9.4    val proof_of_term: theory -> bool -> term -> Proofterm.proof
     9.5    val term_of_proof: Proofterm.proof -> term
     9.6    val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
     9.7 -  val read_term: theory -> typ -> string -> term
     9.8 -  val read_proof: theory -> bool -> string -> Proofterm.proof
     9.9 +  val strip_sorts_consttypes: Proof.context -> Proof.context
    9.10 +  val read_term: theory -> bool -> typ -> string -> term
    9.11 +  val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
    9.12    val proof_syntax: Proofterm.proof -> theory -> theory
    9.13    val proof_of: bool -> thm -> Proofterm.proof
    9.14    val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
    9.15 @@ -109,7 +110,7 @@
    9.16               | "thm" :: xs =>
    9.17                   let val name = Long_Name.implode xs;
    9.18                   in (case AList.lookup (op =) thms name of
    9.19 -                     SOME thm => fst (strip_combt (Thm.proof_of thm))
    9.20 +                     SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm))))
    9.21                     | NONE => error ("Unknown theorem " ^ quote name))
    9.22                   end
    9.23               | _ => error ("Illegal proof constant name: " ^ quote s))
    9.24 @@ -198,7 +199,14 @@
    9.25      (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
    9.26    end;
    9.27  
    9.28 -fun read_term thy =
    9.29 +fun strip_sorts_consttypes ctxt =
    9.30 +  let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt)
    9.31 +  in Symtab.fold (fn (s, (T, _)) =>
    9.32 +      ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T)))
    9.33 +    tab ctxt
    9.34 +  end;
    9.35 +
    9.36 +fun read_term thy topsort =
    9.37    let
    9.38      val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
    9.39      val axm_names = map fst (Theory.all_axioms_of thy);
    9.40 @@ -208,15 +216,19 @@
    9.41          (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
    9.42        |> ProofContext.init_global
    9.43        |> ProofContext.allow_dummies
    9.44 -      |> ProofContext.set_mode ProofContext.mode_schematic;
    9.45 +      |> ProofContext.set_mode ProofContext.mode_schematic
    9.46 +      |> (if topsort then
    9.47 +            strip_sorts_consttypes #>
    9.48 +            ProofContext.set_defsort []
    9.49 +          else I);
    9.50    in
    9.51      fn ty => fn s =>
    9.52        (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
    9.53        |> Type_Infer.constrain ty |> Syntax.check_term ctxt
    9.54    end;
    9.55  
    9.56 -fun read_proof thy =
    9.57 -  let val rd = read_term thy proofT
    9.58 +fun read_proof thy topsort =
    9.59 +  let val rd = read_term thy topsort proofT
    9.60    in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
    9.61  
    9.62  fun proof_syntax prf =
    10.1 --- a/src/Pure/Proof/proofchecker.ML	Tue Jun 01 11:18:51 2010 +0200
    10.2 +++ b/src/Pure/Proof/proofchecker.ML	Tue Jun 01 11:30:57 2010 +0200
    10.3 @@ -28,6 +28,48 @@
    10.4  val beta_eta_convert =
    10.5    Conv.fconv_rule Drule.beta_eta_conversion;
    10.6  
    10.7 +(* equality modulo renaming of type variables *)
    10.8 +fun is_equal t t' =
    10.9 +  let
   10.10 +    val atoms = fold_types (fold_atyps (insert (op =))) t [];
   10.11 +    val atoms' = fold_types (fold_atyps (insert (op =))) t' []
   10.12 +  in
   10.13 +    length atoms = length atoms' andalso
   10.14 +    map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
   10.15 +  end;
   10.16 +
   10.17 +fun pretty_prf thy vs Hs prf =
   10.18 +  let val prf' = prf |> prf_subst_bounds (map Free vs) |>
   10.19 +    prf_subst_pbounds (map (Hyp o prop_of) Hs)
   10.20 +  in
   10.21 +    (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
   10.22 +     Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
   10.23 +  end;
   10.24 +
   10.25 +fun pretty_term thy vs _ t =
   10.26 +  let val t' = subst_bounds (map Free vs, t)
   10.27 +  in
   10.28 +    (Syntax.pretty_term_global thy t',
   10.29 +     Syntax.pretty_typ_global thy (fastype_of t'))
   10.30 +  end;
   10.31 +
   10.32 +fun appl_error thy prt vs Hs s f a =
   10.33 +  let
   10.34 +    val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
   10.35 +    val (pp_a, pp_aT) = prt thy vs Hs a
   10.36 +  in
   10.37 +    error (cat_lines
   10.38 +      [s,
   10.39 +       "",
   10.40 +       Pretty.string_of (Pretty.block
   10.41 +         [Pretty.str "Operator:", Pretty.brk 2, pp_f,
   10.42 +           Pretty.str " ::", Pretty.brk 1, pp_fT]),
   10.43 +       Pretty.string_of (Pretty.block
   10.44 +         [Pretty.str "Operand:", Pretty.brk 3, pp_a,
   10.45 +           Pretty.str " ::", Pretty.brk 1, pp_aT]),
   10.46 +       ""])
   10.47 +  end;
   10.48 +
   10.49  fun thm_of_proof thy prf =
   10.50    let
   10.51      val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
   10.52 @@ -45,9 +87,9 @@
   10.53  
   10.54      fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
   10.55            let
   10.56 -            val thm = Drule.implies_intr_hyps (lookup name);
   10.57 +            val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
   10.58              val {prop, ...} = rep_thm thm;
   10.59 -            val _ = if prop aconv prop' then () else
   10.60 +            val _ = if is_equal prop prop' then () else
   10.61                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
   10.62                  Syntax.string_of_term_global thy prop ^ "\n\n" ^
   10.63                  Syntax.string_of_term_global thy prop');
   10.64 @@ -70,7 +112,10 @@
   10.65            let
   10.66              val thm = thm_of (vs, names) Hs prf;
   10.67              val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
   10.68 -          in Thm.forall_elim ct thm end
   10.69 +          in
   10.70 +            Thm.forall_elim ct thm
   10.71 +            handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
   10.72 +          end
   10.73  
   10.74        | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
   10.75            let
   10.76 @@ -86,6 +131,7 @@
   10.77              val thm' = beta_eta_convert (thm_of vars Hs prf');
   10.78            in
   10.79              Thm.implies_elim thm thm'
   10.80 +            handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
   10.81            end
   10.82  
   10.83        | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
    11.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Jun 01 11:18:51 2010 +0200
    11.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Jun 01 11:30:57 2010 +0200
    11.3 @@ -28,11 +28,7 @@
    11.4  fun forall_intr_vfs prop = fold_rev Logic.all
    11.5    (vars_of prop @ frees_of prop) prop;
    11.6  
    11.7 -fun forall_intr_prf t prf =
    11.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    11.9 -  in Abst (a, SOME T, prf_abstract_over t prf) end;
   11.10 -
   11.11 -fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
   11.12 +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
   11.13    (vars_of prop @ frees_of prop) prf;
   11.14  
   11.15  
    12.1 --- a/src/Pure/axclass.ML	Tue Jun 01 11:18:51 2010 +0200
    12.2 +++ b/src/Pure/axclass.ML	Tue Jun 01 11:30:57 2010 +0200
    12.3 @@ -24,8 +24,8 @@
    12.4    val read_classrel: theory -> xstring * xstring -> class * class
    12.5    val declare_overloaded: string * typ -> theory -> term * theory
    12.6    val define_overloaded: binding -> string * term -> theory -> thm * theory
    12.7 -  val add_classrel: thm -> theory -> theory
    12.8 -  val add_arity: thm -> theory -> theory
    12.9 +  val add_classrel: bool -> thm -> theory -> theory
   12.10 +  val add_arity: bool -> thm -> theory -> theory
   12.11    val prove_classrel: class * class -> tactic -> theory -> theory
   12.12    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
   12.13    val define_class: binding * class list -> string list ->
   12.14 @@ -412,46 +412,55 @@
   12.15  
   12.16  (* primitive rules *)
   12.17  
   12.18 -fun add_classrel raw_th thy =
   12.19 +fun add_classrel store raw_th thy =
   12.20    let
   12.21      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   12.22      val prop = Thm.plain_prop_of th;
   12.23      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
   12.24      val rel = Logic.dest_classrel prop handle TERM _ => err ();
   12.25      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   12.26 -    val th' = th
   12.27 +    val (th', thy') =
   12.28 +      if store then PureThy.store_thm
   12.29 +        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
   12.30 +      else (th, thy);
   12.31 +    val th'' = th'
   12.32        |> Thm.unconstrainT
   12.33 -      |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [];
   12.34 +      |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   12.35    in
   12.36 -    thy
   12.37 +    thy'
   12.38      |> Sign.primitive_classrel (c1, c2)
   12.39 -    |> (#2 oo put_trancl_classrel) ((c1, c2), th')
   12.40 +    |> (#2 oo put_trancl_classrel) ((c1, c2), th'')
   12.41      |> perhaps complete_arities
   12.42    end;
   12.43  
   12.44 -fun add_arity raw_th thy =
   12.45 +fun add_arity store raw_th thy =
   12.46    let
   12.47      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   12.48      val prop = Thm.plain_prop_of th;
   12.49      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   12.50 -    val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   12.51 +    val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   12.52 +
   12.53 +    val (th', thy') =
   12.54 +      if store then PureThy.store_thm
   12.55 +        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
   12.56 +      else (th, thy);
   12.57  
   12.58      val args = Name.names Name.context Name.aT Ss;
   12.59      val T = Type (t, map TFree args);
   12.60 -    val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), [])))) args;
   12.61 +    val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
   12.62  
   12.63 -    val missing_params = Sign.complete_sort thy [c]
   12.64 -      |> maps (these o Option.map #params o try (get_info thy))
   12.65 -      |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
   12.66 +    val missing_params = Sign.complete_sort thy' [c]
   12.67 +      |> maps (these o Option.map #params o try (get_info thy'))
   12.68 +      |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t))
   12.69        |> (map o apsnd o map_atyps) (K T);
   12.70 -    val th' = th
   12.71 +    val th'' = th'
   12.72        |> Thm.unconstrainT
   12.73        |> Drule.instantiate' std_vars [];
   12.74    in
   12.75 -    thy
   12.76 +    thy'
   12.77      |> fold (#2 oo declare_overloaded) missing_params
   12.78      |> Sign.primitive_arity (t, Ss, [c])
   12.79 -    |> put_arity ((t, Ss, c), th')
   12.80 +    |> put_arity ((t, Ss, c), th'')
   12.81    end;
   12.82  
   12.83  
   12.84 @@ -468,7 +477,7 @@
   12.85      thy
   12.86      |> PureThy.add_thms [((Binding.name
   12.87          (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
   12.88 -    |-> (fn [th'] => add_classrel th')
   12.89 +    |-> (fn [th'] => add_classrel false th')
   12.90    end;
   12.91  
   12.92  fun prove_arity raw_arity tac thy =
   12.93 @@ -484,7 +493,7 @@
   12.94    in
   12.95      thy
   12.96      |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
   12.97 -    |-> fold add_arity
   12.98 +    |-> fold (add_arity false)
   12.99    end;
  12.100  
  12.101  
  12.102 @@ -618,11 +627,11 @@
  12.103  
  12.104  fun ax_classrel prep =
  12.105    axiomatize (map o prep) (map Logic.mk_classrel)
  12.106 -    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
  12.107 +    (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false);
  12.108  
  12.109  fun ax_arity prep =
  12.110    axiomatize (prep o ProofContext.init_global) Logic.mk_arities
  12.111 -    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
  12.112 +    (map (prefix arity_prefix) o Logic.name_arities) (add_arity false);
  12.113  
  12.114  fun class_const c =
  12.115    (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
    13.1 --- a/src/Pure/logic.ML	Tue Jun 01 11:18:51 2010 +0200
    13.2 +++ b/src/Pure/logic.ML	Tue Jun 01 11:30:57 2010 +0200
    13.3 @@ -46,7 +46,8 @@
    13.4    val name_arity: string * sort list * class -> string
    13.5    val mk_arities: arity -> term list
    13.6    val dest_arity: term -> string * sort list * class
    13.7 -  val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
    13.8 +  val unconstrainT: sort list -> term -> 
    13.9 +    ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
   13.10    val protectC: term
   13.11    val protect: term -> term
   13.12    val unprotect: term -> term
   13.13 @@ -299,11 +300,15 @@
   13.14          map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
   13.15          constraints_map;
   13.16  
   13.17 +    val outer_constraints =
   13.18 +      maps (fn (T, S) => map (pair T) S)
   13.19 +        (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
   13.20 +
   13.21      val prop' =
   13.22        prop
   13.23        |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
   13.24        |> curry list_implies (map snd constraints);
   13.25 -  in ((atyp_map, constraints), prop') end;
   13.26 +  in ((atyp_map, constraints, outer_constraints), prop') end;
   13.27  
   13.28  
   13.29  
    14.1 --- a/src/Pure/proofterm.ML	Tue Jun 01 11:18:51 2010 +0200
    14.2 +++ b/src/Pure/proofterm.ML	Tue Jun 01 11:30:57 2010 +0200
    14.3 @@ -58,6 +58,8 @@
    14.4    val strip_combt: proof -> proof * term option list
    14.5    val strip_combP: proof -> proof * proof list
    14.6    val strip_thm: proof_body -> proof_body
    14.7 +  val map_proof_same: term Same.operation -> typ Same.operation
    14.8 +    -> (typ * class -> proof) -> proof Same.operation
    14.9    val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
   14.10    val map_proof_types_same: typ Same.operation -> proof Same.operation
   14.11    val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
   14.12 @@ -80,7 +82,9 @@
   14.13  
   14.14    (** proof terms for specific inference rules **)
   14.15    val implies_intr_proof: term -> proof -> proof
   14.16 +  val implies_intr_proof': term -> proof -> proof
   14.17    val forall_intr_proof: term -> string -> proof -> proof
   14.18 +  val forall_intr_proof': term -> proof -> proof
   14.19    val varify_proof: term -> (string * sort) list -> proof -> proof
   14.20    val legacy_freezeT: term -> proof -> proof
   14.21    val rotate_proof: term list -> term -> int -> proof -> proof
   14.22 @@ -121,13 +125,13 @@
   14.23  
   14.24    (** rewriting on proof terms **)
   14.25    val add_prf_rrule: proof * proof -> theory -> theory
   14.26 -  val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
   14.27 +  val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
   14.28    val no_skel: proof
   14.29    val normal_skel: proof
   14.30    val rewrite_proof: theory -> (proof * proof) list *
   14.31 -    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
   14.32 +    (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   14.33    val rewrite_proof_notypes: (proof * proof) list *
   14.34 -    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
   14.35 +    (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   14.36    val rew_proof: theory -> proof -> proof
   14.37  
   14.38    val promise_proof: theory -> serial -> term -> proof
   14.39 @@ -618,7 +622,7 @@
   14.40  
   14.41  (***** implication introduction *****)
   14.42  
   14.43 -fun implies_intr_proof h prf =
   14.44 +fun gen_implies_intr_proof f h prf =
   14.45    let
   14.46      fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME
   14.47        | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
   14.48 @@ -630,14 +634,21 @@
   14.49        | abshyp _ _ = raise Same.SAME
   14.50      and abshyph i prf = (abshyp i prf handle Same.SAME => prf);
   14.51    in
   14.52 -    AbsP ("H", NONE (*h*), abshyph 0 prf)
   14.53 +    AbsP ("H", f h, abshyph 0 prf)
   14.54    end;
   14.55  
   14.56 +val implies_intr_proof = gen_implies_intr_proof (K NONE);
   14.57 +val implies_intr_proof' = gen_implies_intr_proof SOME;
   14.58 +
   14.59  
   14.60  (***** forall introduction *****)
   14.61  
   14.62  fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
   14.63  
   14.64 +fun forall_intr_proof' t prf =
   14.65 +  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   14.66 +  in Abst (a, SOME T, prf_abstract_over t prf) end;
   14.67 +
   14.68  
   14.69  (***** varify *****)
   14.70  
   14.71 @@ -1105,7 +1116,7 @@
   14.72  
   14.73  fun flt (i: int) = filter (fn n => n < i);
   14.74  
   14.75 -fun fomatch Ts tymatch j =
   14.76 +fun fomatch Ts tymatch j instsp p =
   14.77    let
   14.78      fun mtch (instsp as (tyinsts, insts)) = fn
   14.79          (Var (ixn, T), t)  =>
   14.80 @@ -1120,7 +1131,7 @@
   14.81        | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
   14.82        | (Bound i, Bound j) => if i=j then instsp else raise PMatch
   14.83        | _ => raise PMatch
   14.84 -  in mtch end;
   14.85 +  in mtch instsp (pairself Envir.beta_eta_contract p) end;
   14.86  
   14.87  fun match_proof Ts tymatch =
   14.88    let
   14.89 @@ -1253,72 +1264,72 @@
   14.90  
   14.91  fun rewrite_prf tymatch (rules, procs) prf =
   14.92    let
   14.93 -    fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
   14.94 -      | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
   14.95 -      | rew Ts prf =
   14.96 -          (case get_first (fn r => r Ts prf) procs of
   14.97 +    fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
   14.98 +      | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
   14.99 +      | rew Ts hs prf =
  14.100 +          (case get_first (fn r => r Ts hs prf) procs of
  14.101              NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
  14.102                (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
  14.103                   handle PMatch => NONE) (filter (could_unify prf o fst) rules)
  14.104            | some => some);
  14.105  
  14.106 -    fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
  14.107 -          if prf_loose_Pbvar1 prf' 0 then rew Ts prf
  14.108 +    fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
  14.109 +          if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf
  14.110            else
  14.111              let val prf'' = incr_pboundvars (~1) 0 prf'
  14.112 -            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
  14.113 -      | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
  14.114 -          if prf_loose_bvar1 prf' 0 then rew Ts prf
  14.115 +            in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
  14.116 +      | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) =
  14.117 +          if prf_loose_bvar1 prf' 0 then rew Ts hs prf
  14.118            else
  14.119              let val prf'' = incr_pboundvars 0 (~1) prf'
  14.120 -            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
  14.121 -      | rew0 Ts prf = rew Ts prf;
  14.122 +            in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
  14.123 +      | rew0 Ts hs prf = rew Ts hs prf;
  14.124  
  14.125 -    fun rew1 _ (Hyp (Var _)) _ = NONE
  14.126 -      | rew1 Ts skel prf = (case rew2 Ts skel prf of
  14.127 -          SOME prf1 => (case rew0 Ts prf1 of
  14.128 -              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2))
  14.129 +    fun rew1 _ _ (Hyp (Var _)) _ = NONE
  14.130 +      | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
  14.131 +          SOME prf1 => (case rew0 Ts hs prf1 of
  14.132 +              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
  14.133              | NONE => SOME prf1)
  14.134 -        | NONE => (case rew0 Ts prf of
  14.135 -              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1))
  14.136 +        | NONE => (case rew0 Ts hs prf of
  14.137 +              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
  14.138              | NONE => NONE))
  14.139  
  14.140 -    and rew2 Ts skel (prf % SOME t) = (case prf of
  14.141 +    and rew2 Ts hs skel (prf % SOME t) = (case prf of
  14.142              Abst (_, _, body) =>
  14.143                let val prf' = prf_subst_bounds [t] body
  14.144 -              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
  14.145 -          | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
  14.146 +              in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
  14.147 +          | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
  14.148                SOME prf' => SOME (prf' % SOME t)
  14.149              | NONE => NONE))
  14.150 -      | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
  14.151 -          (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
  14.152 -      | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
  14.153 +      | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
  14.154 +          (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
  14.155 +      | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
  14.156              AbsP (_, _, body) =>
  14.157                let val prf' = prf_subst_pbounds [prf2] body
  14.158 -              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
  14.159 +              in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
  14.160            | _ =>
  14.161              let val (skel1, skel2) = (case skel of
  14.162                  skel1 %% skel2 => (skel1, skel2)
  14.163                | _ => (no_skel, no_skel))
  14.164 -            in case rew1 Ts skel1 prf1 of
  14.165 -                SOME prf1' => (case rew1 Ts skel2 prf2 of
  14.166 +            in case rew1 Ts hs skel1 prf1 of
  14.167 +                SOME prf1' => (case rew1 Ts hs skel2 prf2 of
  14.168                      SOME prf2' => SOME (prf1' %% prf2')
  14.169                    | NONE => SOME (prf1' %% prf2))
  14.170 -              | NONE => (case rew1 Ts skel2 prf2 of
  14.171 +              | NONE => (case rew1 Ts hs skel2 prf2 of
  14.172                      SOME prf2' => SOME (prf1 %% prf2')
  14.173                    | NONE => NONE)
  14.174              end)
  14.175 -      | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
  14.176 +      | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
  14.177                (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
  14.178              SOME prf' => SOME (Abst (s, T, prf'))
  14.179            | NONE => NONE)
  14.180 -      | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
  14.181 +      | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
  14.182                (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
  14.183              SOME prf' => SOME (AbsP (s, t, prf'))
  14.184            | NONE => NONE)
  14.185 -      | rew2 _ _ _ = NONE;
  14.186 +      | rew2 _ _ _ _ = NONE;
  14.187  
  14.188 -  in the_default prf (rew1 [] no_skel prf) end;
  14.189 +  in the_default prf (rew1 [] [] no_skel prf) end;
  14.190  
  14.191  fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
  14.192    Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
  14.193 @@ -1332,7 +1343,7 @@
  14.194  (
  14.195    type T =
  14.196      (stamp * (proof * proof)) list *
  14.197 -    (stamp * (typ list -> proof -> (proof * proof) option)) list;
  14.198 +    (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list;
  14.199  
  14.200    val empty = ([], []);
  14.201    val extend = I;
  14.202 @@ -1373,7 +1384,7 @@
  14.203            | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
  14.204        | fill _ = NONE;
  14.205      val (rules, procs) = get_data thy;
  14.206 -    val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
  14.207 +    val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
  14.208    in PBody {oracles = oracles, thms = thms, proof = proof} end;
  14.209  
  14.210  fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
  14.211 @@ -1421,12 +1432,13 @@
  14.212      val (postproc, ofclasses, prop1, args1) =
  14.213        if do_unconstrain then
  14.214          let
  14.215 -          val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
  14.216 +          val ((atyp_map, constraints, outer_constraints), prop1) =
  14.217 +            Logic.unconstrainT shyps prop;
  14.218            val postproc = unconstrainT_body thy (atyp_map, constraints);
  14.219            val args1 =
  14.220              (map o Option.map o Term.map_types o Term.map_atyps)
  14.221                (Type.strip_sorts o atyp_map) args;
  14.222 -        in (postproc, map (OfClass o fst) constraints, prop1, args1) end
  14.223 +        in (postproc, map OfClass outer_constraints, prop1, args1) end
  14.224        else (I, [], prop, args);
  14.225      val argsP = ofclasses @ map Hyp hyps;
  14.226  
  14.227 @@ -1447,7 +1459,7 @@
  14.228      val head = PThm (i, ((name, prop1, NONE), body'));
  14.229    in ((i, (name, prop1, body')), head, args, argsP, args1) end;
  14.230  
  14.231 -val unconstrain_thm_proofs = Unsynchronized.ref false;
  14.232 +val unconstrain_thm_proofs = Unsynchronized.ref true;
  14.233  
  14.234  fun thm_proof thy name shyps hyps concl promises body =
  14.235    let val (pthm, head, args, argsP, _) =
    15.1 --- a/src/Pure/type_infer.ML	Tue Jun 01 11:18:51 2010 +0200
    15.2 +++ b/src/Pure/type_infer.ML	Tue Jun 01 11:30:57 2010 +0200
    15.3 @@ -295,11 +295,11 @@
    15.4        | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
    15.5        | occurs_check _ _ _ = ();
    15.6  
    15.7 -    fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) =
    15.8 +    fun assign i (T as Param (i', _)) S tye_idx =
    15.9            if i = i' then tye_idx
   15.10 -          else meet (T, S) (Inttab.update_new (i, T) tye, idx)
   15.11 -      | assign i T S (tye, idx) =
   15.12 -          (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx));
   15.13 +          else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
   15.14 +      | assign i T S (tye_idx as (tye, _)) =
   15.15 +          (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
   15.16  
   15.17  
   15.18      (* unification *)