Mercurial Mercurial > repos > isabelle / 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.
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51908 5aaa9e2f7dd1
parent 51907 882d850aa3ca
child 51910 31bb70ddee7e 
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 17:29:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 17:35:29 2013 +0200
@@ -480,7 +480,6 @@
         val spec =
           mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
             mk_iter_body lthy0 fpTs ctor_iter fss xsss);
-val _ = tracing ("*** spec: " ^ Syntax.string_of_term lthy0 spec) (*###*)
       in (binding, spec) end;
 
     val binding_specs =
isabelle