src/Pure/thm.ML
changeset 32032 a6a6e8031c14
parent 32027 9dd548810ed1
child 32035 8e77b6a250d5
     1.1 --- a/src/Pure/thm.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -1247,12 +1247,12 @@
     1.4      val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
     1.5      val thy = Theory.deref thy_ref;
     1.6      val (tpairs, Bs, Bi, C) = dest_state (state, i);
     1.7 -    fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
     1.8 +    fun newth n (env, tpairs) =
     1.9        Thm (deriv_rule1
    1.10            ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
    1.11              Pt.assumption_proof Bs Bi n) der,
    1.12         {tags = [],
    1.13 -        maxidx = maxidx,
    1.14 +        maxidx = Envir.maxidx_of env,
    1.15          shyps = Envir.insert_sorts env shyps,
    1.16          hyps = hyps,
    1.17          tpairs =
    1.18 @@ -1465,15 +1465,15 @@
    1.19  
    1.20  (*Faster normalization: skip assumptions that were lifted over*)
    1.21  fun norm_term_skip env 0 t = Envir.norm_term env t
    1.22 -  | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
    1.23 -        let val Envir.Envir{iTs, ...} = env
    1.24 -            val T' = Envir.typ_subst_TVars iTs T
    1.25 -            (*Must instantiate types of parameters because they are flattened;
    1.26 -              this could be a NEW parameter*)
    1.27 -        in Term.all T' $ Abs(a, T', norm_term_skip env n t)  end
    1.28 -  | norm_term_skip env n (Const("==>", _) $ A $ B) =
    1.29 -        Logic.mk_implies (A, norm_term_skip env (n-1) B)
    1.30 -  | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
    1.31 +  | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
    1.32 +      let
    1.33 +        val T' = Envir.typ_subst_TVars (Envir.type_env env) T
    1.34 +        (*Must instantiate types of parameters because they are flattened;
    1.35 +          this could be a NEW parameter*)
    1.36 +      in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
    1.37 +  | norm_term_skip env n (Const ("==>", _) $ A $ B) =
    1.38 +      Logic.mk_implies (A, norm_term_skip env (n - 1) B)
    1.39 +  | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
    1.40  
    1.41  
    1.42  (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
    1.43 @@ -1495,7 +1495,7 @@
    1.44       and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
    1.45       val thy = Theory.deref (merge_thys2 state orule);
    1.46       (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
    1.47 -     fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
    1.48 +     fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
    1.49         let val normt = Envir.norm_term env;
    1.50             (*perform minimal copying here by examining env*)
    1.51             val (ntpairs, normp) =
    1.52 @@ -1520,7 +1520,7 @@
    1.53                         curry op oo (Pt.norm_proof' env))
    1.54                      (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
    1.55                  {tags = [],
    1.56 -                 maxidx = maxidx,
    1.57 +                 maxidx = Envir.maxidx_of env,
    1.58                   shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
    1.59                   hyps = union_hyps rhyps shyps,
    1.60                   tpairs = ntpairs,