--- a/Nominal/Nominal2.thy	Wed Jan 19 07:06:47 2011 +0100
+++ b/Nominal/Nominal2.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -653,7 +653,7 @@
 
   val bclauses' = complete dt_strs bclauses
 in
-  timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy)
+  nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy
 end
 *}
 
@@ -705,10 +705,11 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
+(*
 ML {*
 trace := true
 *}
-
+*)
 
 end