src/Provers/quasi.ML
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 *)