--- a/Quot/Examples/IntEx2.thy	Thu Dec 10 05:11:53 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 08:44:01 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx2
-imports "../QuotMain" Nat Presburger
+imports "../QuotMain" Nat
 (*uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
@@ -89,7 +89,7 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 by auto
 
-lemma minus_raw_rsp[quot_respect]:
+lemma uminus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
   by auto
 
@@ -172,10 +172,6 @@
 
 text{* The integers form a @{text comm_ring_1}*}
 
-ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *}
-ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *}
-ML {* @{term "0 :: int"} *}
-
 instance int :: comm_ring_1
 proof
   fix i j k :: int