killed internal output
authortraytel
Mon, 03 Sep 2012 18:12:59 +0200
changeset 49105 a426099dc343
parent 49104 6defdacd595a
child 49106 aa09d99bf414
killed internal output
src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 03 17:57:34 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 03 18:12:59 2012 +0200
@@ -2766,9 +2766,6 @@
         val coind_witss =
           maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
 
-        val _ = (warning o PolyML.makestring) (map length coind_wit_argsss)
-        val _ = (warning o PolyML.makestring) (map length nonredundant_coind_wit_argsss)
-
         fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
           let
             fun mk_goal sets y y_copy y'_copy j =