Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2.thy
changeset 2643 0579d3a48304
parent 2640 75d353e8e60e
child 2647 5e95387bef45 
--- a/Nominal/Nominal2.thy	Thu Jan 06 13:28:19 2011 +0000
+++ b/Nominal/Nominal2.thy	Thu Jan 06 13:28:40 2011 +0000
@@ -154,8 +154,6 @@
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses 
 
-  val _ = tracing ("raw_dt info:\n" ^ @{make_string} raw_dts)
-
   val (raw_dt_full_names, thy1) = 
     Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
nominal2