src/Provers/order.ML

--- a/src/Provers/order.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/Provers/order.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 *)