src/Tools/eqsubst.ML
changeset 59621 291934bac95e
parent 59498 50b60f501b05
child 59642 929984c529d3
     1.1 --- a/src/Tools/eqsubst.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -260,7 +260,7 @@
     1.4      val tgt_term = Thm.prop_of th;
     1.5  
     1.6      val thy = Thm.theory_of_thm th;
     1.7 -    val cert = Thm.cterm_of thy;
     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 @@ -349,7 +349,7 @@
    1.13      val tgt_term = Thm.prop_of th;
    1.14  
    1.15      val thy = Thm.theory_of_thm th;
    1.16 -    val cert = Thm.cterm_of thy;
    1.17 +    val cert = Thm.global_cterm_of thy;
    1.18  
    1.19      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    1.20      val cfvs = rev (map cert fvs);