diff -r 5c1e6b896ff0 -r 2c95d0436a2b IntEx2.thy
--- a/IntEx2.thy	Mon Dec 07 00:13:36 2009 +0100
+++ b/IntEx2.thy	Mon Dec 07 01:22:20 2009 +0100
@@ -389,6 +389,7 @@
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
 use "~~/src/HOL/Tools/numeral_syntax.ML"
+(*
 setup NumeralSyntax.setup
 
 abbreviation
@@ -432,3 +433,4 @@
 
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
+*)
\ No newline at end of file