src/Provers/splitter.ML
changeset 22578 b0eb5652f210
parent 21879 a3efbae45735
child 22596 d0d2af4db18f
     1.1 --- a/src/Provers/splitter.ML	Wed Apr 04 00:10:59 2007 +0200
     1.2 +++ b/src/Provers/splitter.ML	Wed Apr 04 00:11:03 2007 +0200
     1.3 @@ -322,7 +322,7 @@
     1.4  
     1.5  fun inst_lift Ts t (T, U, pos) state i =
     1.6    let
     1.7 -    val cert = cterm_of (sign_of_thm state);
     1.8 +    val cert = cterm_of (Thm.theory_of_thm state);
     1.9      val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));
    1.10    in cterm_instantiate [(cert P, cert cntxt)] trlift
    1.11    end;
    1.12 @@ -346,7 +346,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 (#prop (rep_thm thm')))));
    1.16 -    val cert = cterm_of (sign_of_thm state);
    1.17 +    val cert = cterm_of (Thm.theory_of_thm state);
    1.18      val cntxt = mk_cntxt_splitthm t tt TB;
    1.19      val abss = Library.foldl (fn (t, T) => Abs ("", T, t));
    1.20    in cterm_instantiate [(cert P, cert (abss (cntxt, Ts)))] thm'