Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Integ/Int.ML
changeset 9436 62bb04ab4b01
parent 8785 00cff9d083df
child 9582 38e58ed53e7b 
--- a/src/HOL/Integ/Int.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/Int.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -34,7 +34,7 @@
   val ss		= HOL_ss
   val eq_reflection	= eq_reflection
 
-  val thy	= IntDef.thy
+  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context ()))
   val T		= HOLogic.intT
   val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
   val restrict_to_left  = restrict_to_left
isabelle