diff -r 1a08fce38565 -r b0eb5652f210 src/HOL/Real/float.ML
--- a/src/HOL/Real/float.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Real/float.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -424,7 +424,7 @@
 fun invoke_float_op c =
     let
 	val th = (if length(!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
-	val sg = (if length(!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
+	val sg = (if length(!sg) = 0 then sg := [th] else (); hd (!sg))
     in
 	invoke_oracle th "float_op" (sg, Float_op_oracle_data c)
     end
@@ -463,7 +463,7 @@
 fun invoke_nat_op c =
     let
 	val th = (if length (!th) = 0 then th := [theory "MatrixLP"] else (); hd (!th))
-	val sg = (if length (!sg) = 0 then sg := [sign_of th] else (); hd (!sg))
+	val sg = (if length (!sg) = 0 then sg := [th] else (); hd (!sg))
     in
 	invoke_oracle th "nat_op" (sg, Nat_op_oracle_data c)
     end