# HG changeset patch
# User paulson
# Date 936177335 -7200
# Node ID e53d5f0c7c94838e31fe3b87541de306bd3a1f04
# Parent  e355f626b2f9b280cca5caed0fff21bf33ba949a
tidied

diff -r e355f626b2f9 -r e53d5f0c7c94 src/HOL/Integ/bin_simprocs.ML
--- a/src/HOL/Integ/bin_simprocs.ML	Tue Aug 31 16:04:43 1999 +0200
+++ b/src/HOL/Integ/bin_simprocs.ML	Wed Sep 01 11:15:35 1999 +0200
@@ -26,8 +26,8 @@
 struct
   val ss		= HOL_ss
   val eq_reflection	= eq_reflection
-  val thy	= Bin.thy
-  val T		= Type ("IntDef.int", [])
+  val thy		= Bin.thy
+  val T			= HOLogic.intT
 
   val trans		= trans
   val add_ac		= zadd_ac