diff -r 01a0da807f50 -r 66f39908df95 IntEx2.thy
--- a/IntEx2.thy	Mon Dec 07 04:39:42 2009 +0100
+++ b/IntEx2.thy	Mon Dec 07 04:41:42 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