src/HOL/Integ/presburger.ML

--- a/src/HOL/Integ/presburger.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Integ/presburger.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -281,7 +281,7 @@
 fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
-    val sg = sign_of_thm st
+    val sg = Thm.theory_of_thm st
     (* The Abstraction step *)
     val g' = if a then abstract_pres sg g else g
     (* Transform the term*)