renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
authorwenzelm
Thu Jun 09 23:12:02 2011 +0200 (2011-06-09)
changeset 433332bdec7f430d3
parent 43332 dca2c7c598f0
child 43345 165188299a25
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/reflection.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/split_rule.ML
src/Provers/hypsubst.ML
src/Pure/Isar/rule_insts.ML
src/Pure/conv.ML
src/Pure/drule.ML
src/Tools/induct.ML
src/ZF/Tools/cartprod.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jun 09 22:25:25 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jun 09 23:12:02 2011 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4     fun fw mi th th' th'' =
     1.5       let
     1.6        val th0 = if mi then
     1.7 -           instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
     1.8 -        else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
     1.9 +           Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    1.10 +        else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    1.11       in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    1.12    in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    1.13        fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    1.14 @@ -114,11 +114,11 @@
    1.15     val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
    1.16          pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
    1.17     val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
    1.18 -        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
    1.19 +        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
    1.20     val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
    1.21 -        npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
    1.22 +        npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
    1.23     val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
    1.24 -        ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
    1.25 +        ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
    1.26  
    1.27     fun decomp_mpinf fm =
    1.28       case term_of fm of
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jun 09 22:25:25 2011 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jun 09 23:12:02 2011 +0200
     2.3 @@ -1419,7 +1419,7 @@
     2.4                                  | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
     2.5                               ))
     2.6                           (zip tys_before tys_after)
     2.7 -        val res = Drule.instantiate (tyinst,[]) th1
     2.8 +        val res = Drule.instantiate_normalize (tyinst,[]) th1
     2.9          val hth = HOLThm([],res)
    2.10          val res = norm_hthm thy hth
    2.11          val _ = message "RESULT:"
     3.1 --- a/src/HOL/Import/shuffler.ML	Thu Jun 09 22:25:25 2011 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jun 09 23:12:02 2011 +0200
     3.3 @@ -249,7 +249,7 @@
     3.4          val mid =
     3.5              case rens of
     3.6                  [] => thm'
     3.7 -              | [((_, S), idx)] => instantiate
     3.8 +              | [((_, S), idx)] => Drule.instantiate_normalize
     3.9              ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
    3.10                | _ => error "Shuffler.inst_tfrees internal error"
    3.11      in
     4.1 --- a/src/HOL/Library/reflection.ML	Thu Jun 09 22:25:25 2011 +0200
     4.2 +++ b/src/HOL/Library/reflection.ML	Thu Jun 09 23:12:02 2011 +0200
     4.3 @@ -157,7 +157,7 @@
     4.4                   map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
     4.5                val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
     4.6              in ((fts ~~ (replicate (length fts) ctxt),
     4.7 -                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
     4.8 +                 Library.apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
     4.9              end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
    4.10        end;
    4.11  
    4.12 @@ -230,7 +230,7 @@
    4.13              val substt =
    4.14                let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[]))
    4.15                in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts)  end
    4.16 -            val th = (instantiate (subst_ty, substt)  eq) RS sym
    4.17 +            val th = (Drule.instantiate_normalize (subst_ty, substt)  eq) RS sym
    4.18            in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
    4.19            handle Pattern.MATCH => tryeqs eqs bds)
    4.20        in tryeqs (filter isat eqs) bds end), bds);
    4.21 @@ -277,7 +277,7 @@
    4.22      val cert = cterm_of (Proof_Context.theory_of ctxt)
    4.23      val cvs = map (fn (v as Var(n,t)) => (cert v,
    4.24                    the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
    4.25 -    val th' = instantiate ([], cvs) th
    4.26 +    val th' = Drule.instantiate_normalize ([], cvs) th
    4.27      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
    4.28      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
    4.29                 (fn _ => simp_tac (simpset_of ctxt) 1)
     5.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jun 09 22:25:25 2011 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Thu Jun 09 23:12:02 2011 +0200
     5.3 @@ -306,7 +306,7 @@
     5.4          (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
     5.5  
     5.6    in fst (RealArith.real_linear_prover translator
     5.7 -        (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
     5.8 +        (map (fn t => Drule.instantiate_normalize ([(tv_n, ctyp_of_term t)],[]) pth_zero)
     5.9              zerodests,
    5.10          map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
    5.11                         arg_conv (arg_conv real_poly_conv))) ges',
    5.12 @@ -343,7 +343,7 @@
    5.13    val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
    5.14    val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
    5.15    val cps = map (swap o Thm.dest_equals) (cprems_of th11)
    5.16 -  val th12 = instantiate ([], cps) th11
    5.17 +  val th12 = Drule.instantiate_normalize ([], cps) th11
    5.18    val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
    5.19   in hd (Variable.export ctxt' ctxt [th13])
    5.20   end
     6.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 22:25:25 2011 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Jun 09 23:12:02 2011 +0200
     6.3 @@ -206,7 +206,7 @@
     6.4                     |> map (fn (x, (S, T)) =>
     6.5                                pairself (ctyp_of thy) (TVar (x, S), T)) of
     6.6               [] => raise TERM z
     6.7 -           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
     6.8 +           | ps => aux (Drule.instantiate_normalize (ps, []) tha) (Drule.instantiate_normalize (ps, []) thb)
     6.9    end
    6.10  
    6.11  fun s_not (@{const Not} $ t) = t
    6.12 @@ -562,7 +562,7 @@
    6.13                          tyenv []
    6.14            val t_inst =
    6.15              [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
    6.16 -        in th |> instantiate (ty_inst, t_inst) end
    6.17 +        in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
    6.18        | _ => raise Fail "expected a single non-zapped, non-Metis Var"
    6.19    in
    6.20      (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
     7.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Jun 09 22:25:25 2011 +0200
     7.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Jun 09 23:12:02 2011 +0200
     7.3 @@ -156,10 +156,10 @@
     7.4        [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
     7.5    let
     7.6     val (mp', mq') = (get_pmi th_1, get_pmi th_1')
     7.7 -   val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
     7.8 +   val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
     7.9                     [th_1, th_1']
    7.10 -   val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
    7.11 -   val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
    7.12 +   val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
    7.13 +   val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
    7.14    in (mi_th, set_th, infD_th)
    7.15    end;
    7.16  
     8.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 09 22:25:25 2011 +0200
     8.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 09 23:12:02 2011 +0200
     8.3 @@ -100,7 +100,7 @@
     8.4      val cT_random_aux = inst pt_random_aux;
     8.5      val cT_rhs = inst pt_rhs;
     8.6      val rule = @{thm random_aux_rec}
     8.7 -      |> Drule.instantiate ([(aT, icT)],
     8.8 +      |> Drule.instantiate_normalize ([(aT, icT)],
     8.9             [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
    8.10      val tac = ALLGOALS (rtac rule)
    8.11        THEN ALLGOALS (simp_tac rew_ss)
     9.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jun 09 22:25:25 2011 +0200
     9.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Jun 09 23:12:02 2011 +0200
     9.3 @@ -108,7 +108,7 @@
     9.4      | SOME thm' =>
     9.5          (case try (get_match_inst thy (get_lhs thm')) redex of
     9.6            NONE => NONE
     9.7 -        | SOME inst2 => try (Drule.instantiate inst2) thm'))
     9.8 +        | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
     9.9    end
    9.10  
    9.11  fun ball_bex_range_simproc ss redex =
    9.12 @@ -490,7 +490,7 @@
    9.13            if ty_c = ty_d
    9.14            then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
    9.15            else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
    9.16 -        val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
    9.17 +        val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
    9.18        in
    9.19          Conv.rewr_conv thm4 ctrm
    9.20        end
    10.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Jun 09 22:25:25 2011 +0200
    10.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Jun 09 23:12:02 2011 +0200
    10.3 @@ -270,7 +270,7 @@
    10.4        val gspec = Thm.forall_intr (cterm_of thy x) spec
    10.5  in
    10.6  fun SPEC tm thm =
    10.7 -   let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
    10.8 +   let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_term tm)], []) gspec
    10.9     in thm RS (Thm.forall_elim tm gspec') end
   10.10  end;
   10.11  
   10.12 @@ -298,7 +298,7 @@
   10.13         val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
   10.14         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
   10.15         val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
   10.16 -       val allI2 = instantiate (certify thy theta) allI
   10.17 +       val allI2 = Drule.instantiate_normalize (certify thy theta) allI
   10.18         val thm = Thm.implies_elim allI2 gth
   10.19         val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
   10.20         val prop' = tp $ (A $ Abs(x,ty,M))
    11.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Jun 09 22:25:25 2011 +0200
    11.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Jun 09 23:12:02 2011 +0200
    11.3 @@ -63,9 +63,9 @@
    11.4    let
    11.5      val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
    11.6      and ct = cterm_of thy t
    11.7 -  in instantiate ([], [(cn, ct)]) @{thm le0} end;
    11.8 +  in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
    11.9  
   11.10 -end;  (* LA_Logic *)
   11.11 +end;
   11.12  
   11.13  
   11.14  (* arith context data *)
    12.1 --- a/src/HOL/Tools/split_rule.ML	Thu Jun 09 22:25:25 2011 +0200
    12.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Jun 09 23:12:02 2011 +0200
    12.3 @@ -73,7 +73,7 @@
    12.4          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    12.5          val (vs', insts) = fold mk_tuple ts (vs, []);
    12.6        in
    12.7 -        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    12.8 +        (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    12.9        end
   12.10    | complete_split_rule_var _ x = x;
   12.11  
    13.1 --- a/src/Provers/hypsubst.ML	Thu Jun 09 22:25:25 2011 +0200
    13.2 +++ b/src/Provers/hypsubst.ML	Thu Jun 09 23:12:02 2011 +0200
    13.3 @@ -163,7 +163,7 @@
    13.4            | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
    13.5          val thy = Thm.theory_of_thm rl';
    13.6          val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
    13.7 -      in compose_tac (true, Drule.instantiate (instT,
    13.8 +      in compose_tac (true, Drule.instantiate_normalize (instT,
    13.9          map (pairself (cterm_of thy))
   13.10            [(Var (ixn, Ts ---> U --> body_type T), u),
   13.11             (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
    14.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Jun 09 22:25:25 2011 +0200
    14.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Jun 09 23:12:02 2011 +0200
    14.3 @@ -173,7 +173,7 @@
    14.4          else
    14.5            Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    14.6    in
    14.7 -    Drule.instantiate insts thm |> Rule_Cases.save thm
    14.8 +    Drule.instantiate_normalize insts thm |> Rule_Cases.save thm
    14.9    end;
   14.10  
   14.11  fun read_instantiate_mixed' ctxt (args, concl_args) thm =
   14.12 @@ -323,7 +323,7 @@
   14.13          fun liftpair (cv,ct) =
   14.14                (cterm_fun liftvar cv, cterm_fun liftterm ct)
   14.15          val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
   14.16 -        val rule = Drule.instantiate
   14.17 +        val rule = Drule.instantiate_normalize
   14.18                (map lifttvar envT', map liftpair cenv)
   14.19                (Thm.lift_rule (Thm.cprem_of st i) thm)
   14.20        in
   14.21 @@ -347,7 +347,7 @@
   14.22      val maxidx = Thm.maxidx_of rl;
   14.23      fun cvar xi = cert (Var (xi, propT));
   14.24      val revcut_rl' =
   14.25 -      instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   14.26 +      Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
   14.27          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   14.28    in
   14.29      (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
    15.1 --- a/src/Pure/conv.ML	Thu Jun 09 22:25:25 2011 +0200
    15.2 +++ b/src/Pure/conv.ML	Thu Jun 09 23:12:02 2011 +0200
    15.3 @@ -162,7 +162,7 @@
    15.4      val lhs = Thm.lhs_of rule1;
    15.5      val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    15.6    in
    15.7 -    Drule.instantiate (Thm.match (lhs, ct)) rule2
    15.8 +    Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2
    15.9        handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   15.10    end;
   15.11  
    16.1 --- a/src/Pure/drule.ML	Thu Jun 09 22:25:25 2011 +0200
    16.2 +++ b/src/Pure/drule.ML	Thu Jun 09 23:12:02 2011 +0200
    16.3 @@ -24,7 +24,7 @@
    16.4    val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
    16.5    val implies_elim_list: thm -> thm list -> thm
    16.6    val implies_intr_list: cterm list -> thm -> thm
    16.7 -  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    16.8 +  val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    16.9    val zero_var_indexes_list: thm list -> thm list
   16.10    val zero_var_indexes: thm -> thm
   16.11    val implies_intr_hyps: thm -> thm
   16.12 @@ -821,8 +821,7 @@
   16.13  
   16.14  (*** Instantiate theorem th, reading instantiations in theory thy ****)
   16.15  
   16.16 -(*Version that normalizes the result: Thm.instantiate no longer does that*)
   16.17 -fun instantiate instpair th =
   16.18 +fun instantiate_normalize instpair th =
   16.19    Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
   16.20  
   16.21  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   16.22 @@ -854,7 +853,7 @@
   16.23          let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
   16.24          in (inst ct, inst cu) end
   16.25        fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T))
   16.26 -  in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   16.27 +  in  instantiate_normalize (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   16.28    handle TERM _ =>
   16.29             raise THM("cterm_instantiate: incompatible theories",0,[th])
   16.30         | TYPE (msg, _, _) => raise THM(msg, 0, [th])
    17.1 --- a/src/Tools/induct.ML	Thu Jun 09 22:25:25 2011 +0200
    17.2 +++ b/src/Tools/induct.ML	Thu Jun 09 23:12:02 2011 +0200
    17.3 @@ -588,9 +588,10 @@
    17.4          val concl = Logic.strip_assums_concl goal;
    17.5        in
    17.6          Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
    17.7 -        |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
    17.8 +        |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
    17.9        end
   17.10 -  end handle General.Subscript => Seq.empty;
   17.11 +  end
   17.12 +  handle General.Subscript => Seq.empty;
   17.13  
   17.14  end;
   17.15  
    18.1 --- a/src/ZF/Tools/cartprod.ML	Thu Jun 09 22:25:25 2011 +0200
    18.2 +++ b/src/ZF/Tools/cartprod.ML	Thu Jun 09 23:12:02 2011 +0200
    18.3 @@ -108,7 +108,7 @@
    18.4            val newt = ap_split T1 T2 (Var(v,T'))
    18.5            val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    18.6        in
    18.7 -          remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
    18.8 +          remove_split (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
    18.9                                             cterm newt)]) rl)
   18.10        end
   18.11    | split_rule_var (t,T,rl) = rl;
    19.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Jun 09 22:25:25 2011 +0200
    19.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 09 23:12:02 2011 +0200
    19.3 @@ -493,7 +493,7 @@
    19.4         The name "x.1" comes from the "RS spec" !*)
    19.5       val inst =
    19.6           case elem_frees of [_] => I
    19.7 -            | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
    19.8 +            | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
    19.9                                        cterm_of thy1 elem_tuple)]);
   19.10  
   19.11       (*strip quantifier and the implication*)