diff -r 38aa6b67a80b -r 2bee5ca44ef5 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 21:53:50 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