--- a/src/HOL/Integ/Int.thy Thu Dec 04 21:57:15 2003 +0100
+++ b/src/HOL/Integ/Int.thy Fri Dec 05 10:28:02 2003 +0100
@@ -373,7 +373,6 @@
(*Legacy ML bindings, but no longer the structure Int.*)
ML
{*
-val Int_thy = the_context ()
val zabs_def = thm "zabs_def"
val nat_def = thm "nat_def"