# HG changeset patch
# User wenzelm
# Date 964476172 -7200
# Node ID d2fa043ab24f49efa1abb067f5a97456e3f31979
# Parent  ac20534ce4d1bbbe33810a9170c58fc8c8d2a520
do nat pass theory value, but sg_ref;

diff -r ac20534ce4d1 -r d2fa043ab24f src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Tue Jul 25 00:01:46 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML	Tue Jul 25 00:02:52 2000 +0200
@@ -30,7 +30,7 @@
   val ss		= HOL_ss
   val eq_reflection	= eq_reflection
 
-  val thy		= RealDef.thy
+  val sg_ref		= Sign.self_ref (Theory.sign_of (the_context ()))
   val T			= HOLogic.realT
   val zero		= Const ("0", T)
   val restrict_to_left  = restrict_to_left