# HG changeset patch
# User paulson
# Date 932743698 -7200
# Node ID a30e024791c60127926a53bad1d85f66e499c091
# Parent  5ba8d1e42ca6fd365413d5d45b89d828bf614e24
because intT is now defined in HOLogic

diff -r 5ba8d1e42ca6 -r a30e024791c6 src/HOL/Integ/simproc.ML
--- a/src/HOL/Integ/simproc.ML	Fri Jul 23 17:27:48 1999 +0200
+++ b/src/HOL/Integ/simproc.ML	Fri Jul 23 17:28:18 1999 +0200
@@ -31,7 +31,7 @@
   val eq_reflection	= eq_reflection
 
   val thy	= IntDef.thy
-  val T		= Type ("IntDef.int", [])
+  val T		= HOLogic.intT
   val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
   val add_cancel_21	= zadd_cancel_21
   val add_cancel_end	= zadd_cancel_end