changeset 18023 | 3900037edf3d |
parent 17959 | 8db36a108213 |
child 18145 | 6757627acf59 |
--- a/src/Provers/splitter.ML Fri Oct 28 22:27:46 2005 +0200 +++ b/src/Provers/splitter.ML Fri Oct 28 22:27:47 2005 +0200 @@ -302,7 +302,7 @@ fun inst_split Ts t tt thm TB state i = let - val thm' = Thm.lift_rule (state, i) thm; + val thm' = Thm.lift_rule (Thm.cgoal_of state i) thm; val (P, _) = strip_comb (fst (Logic.dest_equals (Logic.strip_assums_concl (#prop (rep_thm thm'))))); val cert = cterm_of (sign_of_thm state);