removed local clone in the predicate compiler
authorbulwahn
Wed Apr 28 16:45:50 2010 +0200 (2010-04-28)
changeset 36510d716eb002b9f
parent 36509 9cff57fc7113
child 36511 db2953f5887a
removed local clone in the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 28 16:45:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 28 16:45:50 2010 +0200
     1.3 @@ -529,19 +529,19 @@
     1.4      fun instantiate i n {context = ctxt, params = p, prems = prems,
     1.5        asms = a, concl = cl, schematics = s}  =
     1.6        let
     1.7 +        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
     1.8 +        fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
     1.9 +          |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
    1.10          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
    1.11          val case_th = MetaSimplifier.simplify true
    1.12            (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
    1.13          val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
    1.14          val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
    1.15 -        val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty)
    1.16 -        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
    1.17 -        val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.18 -        val case_th' = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl})
    1.19 -        val (_, tenv) = fold (Pattern.match thy) (prems_of case_th' ~~ map prop_of prems') (Vartab.empty, Vartab.empty)
    1.20 -        val inst' = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.21 -        val case_th'' = Thm.instantiate ([], inst') case_th'
    1.22 -        val thesis = case_th'' OF prems'
    1.23 +        val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
    1.24 +          OF (replicate nargs @{thm refl})
    1.25 +        val thesis =
    1.26 +          Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
    1.27 +            OF prems'
    1.28        in
    1.29          (rtac thesis 1)
    1.30        end