author | Christian Urban <urbanc@in.tum.de> |
Wed, 18 Aug 2010 00:23:42 +0800 | |
changeset 2411 | dceaf2d9fedd |
parent 2410 | 2bbdb9c427b5 |
child 2412 | 63f0e7f914dd |
--- 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