--- a/Quot/Examples/IntEx2.thy	Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Tue Dec 08 11:20:01 2009 +0100
@@ -166,10 +166,6 @@
 text{*The integers form a @{text comm_ring_1}*}
 
 
-ML {* val qty = @{typ "int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
-
 instance int :: comm_ring_1
 proof
   fix i j k :: int