src/Tools/eqsubst.ML
changeset 59642 929984c529d3
parent 59621 291934bac95e
child 60358 aebfbcab1eb8
     1.1 --- a/src/Tools/eqsubst.ML	Fri Mar 06 23:55:55 2015 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 06 23:56:43 2015 +0100
     1.3 @@ -259,14 +259,11 @@
     1.4      val th = Thm.incr_indexes 1 gth;
     1.5      val tgt_term = Thm.prop_of th;
     1.6  
     1.7 -    val thy = Thm.theory_of_thm th;
     1.8 -    val cert = Thm.global_cterm_of thy;
     1.9 -
    1.10      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    1.11 -    val cfvs = rev (map cert fvs);
    1.12 +    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
    1.13  
    1.14      val conclterm = Logic.strip_imp_concl fixedbody;
    1.15 -    val conclthm = Thm.trivial (cert conclterm);
    1.16 +    val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
    1.17      val maxidx = Thm.maxidx_of th;
    1.18      val ft =
    1.19        (Zipper.move_down_right (* ==> *)
    1.20 @@ -274,7 +271,7 @@
    1.21         o Zipper.mktop
    1.22         o Thm.prop_of) conclthm
    1.23    in
    1.24 -    ((cfvs, conclthm), (thy, maxidx, ft))
    1.25 +    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
    1.26    end;
    1.27  
    1.28  (* substitute using an object or meta level equality *)