src/HOL/Tools/inductive.ML
changeset 38118 561aa8eb63d3
parent 37957 00e848690339
child 38350 480b2de9927c
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Aug 01 10:15:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Aug 01 10:15:43 2010 +0200
     1.3 @@ -548,15 +548,18 @@
     1.4  
     1.5  fun mk_simp_eq ctxt prop =
     1.6    let
     1.7 -    val (c, args) = strip_comb (HOLogic.dest_Trueprop prop)
     1.8      val ctxt' = Variable.auto_fixes prop ctxt
     1.9 -    val cname = fst (dest_Const c)
    1.10 +    val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
    1.11      val info = the_inductive ctxt cname
    1.12      val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
    1.13 -    val (_, args') = strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq))))
    1.14 +    val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
    1.15 +    val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
    1.16 +      (Vartab.empty, Vartab.empty)
    1.17      val certify = cterm_of (ProofContext.theory_of ctxt)
    1.18 -  in
    1.19 -    cterm_instantiate (map (pairself certify) (args' ~~ args)) eq
    1.20 +    val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
    1.21 +      (Term.add_vars lhs_eq [])
    1.22 +   in
    1.23 +    cterm_instantiate inst eq
    1.24      |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
    1.25        (Simplifier.full_rewrite (simpset_of ctxt))))
    1.26      |> singleton (Variable.export ctxt' ctxt)