src/HOL/Tools/datatype_realizer.ML
changeset 60781 2da59cdf531c
parent 60752 b48830b670a1
child 60826 695cf1fab6cc
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -105,15 +105,17 @@
     1.4          (map (fn ((((i, _), T), U), tname) =>
     1.5            make_pred i U T (mk_proj i is r) (Free (tname, T)))
     1.6              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
     1.7 -    val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
     1.8 -      (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
     1.9 +    val inst =
    1.10 +      map (#1 o dest_Var o head_of)
    1.11 +        (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~
    1.12 +      map (Thm.cterm_of ctxt) ps;
    1.13  
    1.14      val thm =
    1.15        Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
    1.16          (fn prems =>
    1.17             EVERY [
    1.18              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
    1.19 -            resolve_tac ctxt [cterm_instantiate inst induct] 1,
    1.20 +            resolve_tac ctxt [infer_instantiate ctxt inst induct] 1,
    1.21              ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
    1.22              rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
    1.23              REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
    1.24 @@ -190,7 +192,7 @@
    1.25            (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
    1.26          (fn prems =>
    1.27             EVERY [
    1.28 -            resolve_tac ctxt [cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust] 1,
    1.29 +            resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1,
    1.30              ALLGOALS (EVERY'
    1.31                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
    1.32                 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])