src/HOL/Tools/Old_Datatype/old_datatype.ML
changeset 60781 2da59cdf531c
parent 60774 6c28d8ed2488
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -248,10 +248,11 @@
     1.4      fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax)
     1.5          (thy, defs, eqns, rep_congs, dist_lemmas) =
     1.6        let
     1.7 +        val ctxt = Proof_Context.init_global thy;
     1.8          val _ $ (_ $ (cong_f $ _) $ _) = Thm.concl_of arg_cong;
     1.9 -        val rep_const = Thm.global_cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
    1.10 -        val cong' = cterm_instantiate [(Thm.global_cterm_of thy cong_f, rep_const)] arg_cong;
    1.11 -        val dist = cterm_instantiate [(Thm.global_cterm_of thy distinct_f, rep_const)] distinct_lemma;
    1.12 +        val rep_const = Thm.cterm_of ctxt (Const (#Rep_name (#1 typedef), T --> Univ_elT));
    1.13 +        val cong' = infer_instantiate ctxt [(#1 (dest_Var cong_f), rep_const)] arg_cong;
    1.14 +        val dist = infer_instantiate ctxt [(#1 (dest_Var distinct_f), rep_const)] distinct_lemma;
    1.15          val (thy', defs', eqns', _) =
    1.16            fold (make_constr_def typedef T (length constrs))
    1.17              (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
    1.18 @@ -635,8 +636,6 @@
    1.19      val frees =
    1.20        if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
    1.21        else map (Free o apfst fst o dest_Var) Ps;
    1.22 -    val indrule_lemma' =
    1.23 -      cterm_instantiate (map (Thm.global_cterm_of thy6) Ps ~~ map (Thm.global_cterm_of thy6) frees) indrule_lemma;
    1.24  
    1.25      val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
    1.26      val dt_induct =
    1.27 @@ -644,16 +643,22 @@
    1.28        (Logic.strip_imp_prems dt_induct_prop)
    1.29        (Logic.strip_imp_concl dt_induct_prop)
    1.30        (fn {context = ctxt, prems, ...} =>
    1.31 -        EVERY
    1.32 -          [resolve_tac ctxt [indrule_lemma'] 1,
    1.33 -           (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
    1.34 -              Object_Logic.atomize_prems_tac ctxt) 1,
    1.35 -           EVERY (map (fn (prem, r) => (EVERY
    1.36 -             [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
    1.37 -              simp_tac (put_simpset HOL_basic_ss ctxt
    1.38 -                addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
    1.39 -              DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    1.40 -                  (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
    1.41 +        let
    1.42 +          val indrule_lemma' =
    1.43 +            infer_instantiate ctxt
    1.44 +              (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma;
    1.45 +        in
    1.46 +          EVERY
    1.47 +            [resolve_tac ctxt [indrule_lemma'] 1,
    1.48 +             (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
    1.49 +                Object_Logic.atomize_prems_tac ctxt) 1,
    1.50 +             EVERY (map (fn (prem, r) => (EVERY
    1.51 +               [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
    1.52 +                simp_tac (put_simpset HOL_basic_ss ctxt
    1.53 +                  addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
    1.54 +                DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
    1.55 +                    (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]
    1.56 +        end);
    1.57  
    1.58      val ([(_, [dt_induct'])], thy7) =
    1.59        thy6