src/HOL/Tools/datatype_realizer.ML
changeset 59617 b60e65ad13df
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 05 13:28:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 00:00:57 2015 +0100
     1.3 @@ -27,7 +27,6 @@
     1.4  fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
     1.5    let
     1.6      val ctxt = Proof_Context.init_global thy;
     1.7 -    val cert = Thm.cterm_of thy;
     1.8  
     1.9      val recTs = Old_Datatype_Aux.get_rec_types descr;
    1.10      val pnames =
    1.11 @@ -106,11 +105,11 @@
    1.12          (map (fn ((((i, _), T), U), tname) =>
    1.13            make_pred i U T (mk_proj i is r) (Free (tname, T)))
    1.14              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    1.15 -    val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
    1.16 +    val inst = map (apply2 (Thm.cterm_of thy)) (map head_of (HOLogic.dest_conj
    1.17        (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
    1.18  
    1.19      val thm =
    1.20 -      Goal.prove_internal ctxt (map cert prems) (cert concl)
    1.21 +      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems) (Thm.cterm_of thy concl)
    1.22          (fn prems =>
    1.23             EVERY [
    1.24              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
    1.25 @@ -160,7 +159,6 @@
    1.26  fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
    1.27    let
    1.28      val ctxt = Proof_Context.init_global thy;
    1.29 -    val cert = Thm.cterm_of thy;
    1.30      val rT = TFree ("'P", @{sort type});
    1.31      val rT' = TVar (("'P", 0), @{sort type});
    1.32  
    1.33 @@ -187,11 +185,12 @@
    1.34      val y' = Free ("y", T);
    1.35  
    1.36      val thm =
    1.37 -      Goal.prove_internal ctxt (map cert prems)
    1.38 -        (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
    1.39 +      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems)
    1.40 +        (Thm.cterm_of thy
    1.41 +          (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
    1.42          (fn prems =>
    1.43             EVERY [
    1.44 -            rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
    1.45 +            rtac (cterm_instantiate [apply2 (Thm.cterm_of thy) (y, y')] exhaust) 1,
    1.46              ALLGOALS (EVERY'
    1.47                [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
    1.48                 resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])