src/HOL/Tools/datatype_realizer.ML
changeset 59621 291934bac95e
parent 59617 b60e65ad13df
child 59642 929984c529d3
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -105,11 +105,11 @@
     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 thy)) (map head_of (HOLogic.dest_conj
     1.8 +    val inst = map (apply2 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj
     1.9        (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
    1.10  
    1.11      val thm =
    1.12 -      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems) (Thm.cterm_of thy concl)
    1.13 +      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl)
    1.14          (fn prems =>
    1.15             EVERY [
    1.16              rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
    1.17 @@ -185,12 +185,12 @@
    1.18      val y' = Free ("y", T);
    1.19  
    1.20      val thm =
    1.21 -      Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems)
    1.22 -        (Thm.cterm_of thy
    1.23 +      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems)
    1.24 +        (Thm.global_cterm_of thy
    1.25            (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
    1.26          (fn prems =>
    1.27             EVERY [
    1.28 -            rtac (cterm_instantiate [apply2 (Thm.cterm_of thy) (y, y')] exhaust) 1,
    1.29 +            rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, 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)])])