src/HOL/Presburger.thy

--- a/src/HOL/Presburger.thy	Mon Oct 29 17:08:01 2007 +0100
+++ b/src/HOL/Presburger.thy	Tue Oct 30 08:45:54 2007 +0100
@@ -703,6 +703,8 @@
   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   less_number_of
 
+context ring_1
+begin
 
 lemma of_int_num [code func]:
   "of_int k = (if k = 0 then 0 else if k < 0 then
@@ -737,3 +739,5 @@
 qed
 
 end
+
+end