src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
changeset 60781 2da59cdf531c
parent 60757 c09598a97436
child 67334 51a7c90fbf19
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -147,8 +147,8 @@
     1.4        (ts ~~ ts') |> map_filter (fn (t, u) =>
     1.5          (case abstr (getP u) of
     1.6            NONE => NONE
     1.7 -        | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
     1.8 -    val indrule' = cterm_instantiate insts indrule;
     1.9 +        | SOME u' => SOME (t |> getP |> snd |> head_of |> dest_Var |> #1, Thm.cterm_of ctxt u')));
    1.10 +    val indrule' = infer_instantiate ctxt insts indrule;
    1.11    in resolve_tac ctxt [indrule'] i end);
    1.12  
    1.13  
    1.14 @@ -163,9 +163,9 @@
    1.15      val prem' = hd (Thm.prems_of exhaustion);
    1.16      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    1.17      val exhaustion' =
    1.18 -      cterm_instantiate
    1.19 -        [apply2 (Thm.cterm_of ctxt)
    1.20 -          (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
    1.21 +      infer_instantiate ctxt
    1.22 +        [(#1 (dest_Var (head_of lhs)),
    1.23 +          Thm.cterm_of ctxt (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
    1.24          exhaustion;
    1.25    in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
    1.26