# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282062222 -28800
# Node ID dceaf2d9feddb5de1087f97600933bbbbd82eebd
# Parent  2bbdb9c427b5f8c5cac40548557ec61857478b0c
put everything in a "timeit"

diff -r 2bbdb9c427b5 -r dceaf2d9fedd Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed Aug 18 00:19:15 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 18 00:23:42 2010 +0800
@@ -810,7 +810,7 @@
   val bclauses = prepare_bclauses dt_strs lthy2
   val bclauses' = complete dt_strs bclauses 
 in
-  nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd
+  timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd)
 end