diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/Nominal2.thy	Sat Jan 11 23:17:23 2014 +0000
@@ -48,8 +48,6 @@
 
 section{* Interface for nominal_datatype *}
 
-ML {* print_depth 50 *}
-
 ML {*
 fun get_cnstrs dts =
   map snd dts