--- 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 =