src/HOL/Nominal/nominal_datatype.ML
changeset 60781 2da59cdf531c
parent 60754 02924903a6fd
child 60787 12cd198f07af
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -788,8 +788,8 @@
     1.4            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
     1.5          val dist =
     1.6            Drule.export_without_context
     1.7 -            (cterm_instantiate
     1.8 -              [(Thm.global_cterm_of thy distinct_f, rep_const)] Old_Datatype.distinct_lemma);
     1.9 +            (infer_instantiate (Proof_Context.init_global thy)
    1.10 +              [(#1 (dest_Var distinct_f), rep_const)] Old_Datatype.distinct_lemma);
    1.11          val (thy', defs', eqns') = fold (make_constr_def tname T T')
    1.12            (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
    1.13        in
    1.14 @@ -1058,24 +1058,27 @@
    1.15      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma)));
    1.16      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
    1.17        map (Free o apfst fst o dest_Var) Ps;
    1.18 -    val indrule_lemma' = cterm_instantiate
    1.19 -      (map (Thm.global_cterm_of thy8) Ps ~~ map (Thm.global_cterm_of thy8) frees) indrule_lemma;
    1.20  
    1.21      val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
    1.22  
    1.23      val dt_induct_prop = Old_Datatype_Prop.make_ind descr';
    1.24      val dt_induct = Goal.prove_global_future thy8 []
    1.25        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    1.26 -      (fn {prems, context = ctxt} => EVERY
    1.27 -        [resolve_tac ctxt [indrule_lemma'] 1,
    1.28 -         (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
    1.29 -           Object_Logic.atomize_prems_tac ctxt) 1,
    1.30 -         EVERY (map (fn (prem, r) => (EVERY
    1.31 -           [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
    1.32 -            simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
    1.33 -            DEPTH_SOLVE_1
    1.34 -              (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    1.35 -                (prems ~~ constr_defs))]);
    1.36 +      (fn {prems, context = ctxt} =>
    1.37 +        let
    1.38 +          val indrule_lemma' = infer_instantiate ctxt
    1.39 +            (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma;
    1.40 +        in
    1.41 +          EVERY [resolve_tac ctxt [indrule_lemma'] 1,
    1.42 +           (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
    1.43 +             Object_Logic.atomize_prems_tac ctxt) 1,
    1.44 +           EVERY (map (fn (prem, r) => (EVERY
    1.45 +             [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
    1.46 +              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
    1.47 +              DEPTH_SOLVE_1
    1.48 +                (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    1.49 +                  (prems ~~ constr_defs))]
    1.50 +        end);
    1.51  
    1.52      val case_names_induct = Old_Datatype_Data.mk_case_names_induct descr'';
    1.53