--- a/IntEx.thy	Wed Nov 11 10:22:47 2009 +0100
+++ b/IntEx.thy	Wed Nov 11 11:59:22 2009 +0100
@@ -46,10 +46,6 @@
 term PLUS
 thm PLUS_def
 
-ML {* toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; *}
-
-ML {* prop_of @{thm PLUS_def} *}
-
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where