src/HOL/Real/ferrante_rackoff.ML

--- a/src/HOL/Real/ferrante_rackoff.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -76,7 +76,7 @@
   THEN (fn st =>
   let
     val g = nth (prems_of st) (i - 1)
-    val thy = sign_of_thm st
+    val thy = Thm.theory_of_thm st
     (* Transform the term*)
     val (t,np,nh) = prepare_for_linr q g
     (* Some simpsets for dealing with mod div abs and nat*)