changeset 22578 | b0eb5652f210 |
parent 19250 | 932a50e2332f |
child 29276 | 94b1ffec9201 |
--- a/src/Provers/quasi.ML Wed Apr 04 00:10:59 2007 +0200 +++ b/src/Provers/quasi.ML Wed Apr 04 00:11:03 2007 +0200 @@ -77,7 +77,7 @@ (* Extract subgoal with signature *) fun SUBGOAL goalfun i st = - goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st + goalfun (List.nth(prems_of st, i-1), i, Thm.theory_of_thm st) st handle Subscript => Seq.empty; (* Internal datatype for the proof *)