# HG changeset patch
# User traytel
# Date 1346688779 -7200
# Node ID a426099dc343c8e1acaf65dd1175a63d6ce06d7f
# Parent  6defdacd595a4fe07009050377bc37ea3d6e5dde
killed internal output

diff -r 6defdacd595a -r a426099dc343 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 =