Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
do nat pass theory value, but sg_ref;
authorwenzelm
Tue, 25 Jul 2000 00:02:52 +0200
changeset 9434 d2fa043ab24f
parent 9433 ac20534ce4d1
child 9435 c3a13a7d4424
do nat pass theory value, but sg_ref;
src/HOL/Real/RealOrd.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle