src/Provers/splitter.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59970 e9f73d87d904
     1.1 --- a/src/Provers/splitter.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Provers/splitter.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -315,7 +315,7 @@
     1.4  
     1.5  fun inst_lift Ts t (T, U, pos) state i =
     1.6    let
     1.7 -    val cert = Thm.cterm_of (Thm.theory_of_thm state);
     1.8 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
     1.9      val (cntxt, u) = mk_cntxt t pos (T --> U);
    1.10      val trlift' = Thm.lift_rule (Thm.cprem_of state i)
    1.11        (Thm.rename_boundvars abs_lift u trlift);
    1.12 @@ -343,7 +343,7 @@
    1.13      val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
    1.14      val (P, _) = strip_comb (fst (Logic.dest_equals
    1.15        (Logic.strip_assums_concl (Thm.prop_of thm'))));
    1.16 -    val cert = Thm.cterm_of (Thm.theory_of_thm state);
    1.17 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm state);
    1.18      val cntxt = mk_cntxt_splitthm t tt TB;
    1.19    in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm'
    1.20    end;