src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49105 a426099dc343
parent 49104 6defdacd595a
child 49109 0e5b859e1c91
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 03 17:57:34 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 03 18:12:59 2012 +0200
     1.3 @@ -2766,9 +2766,6 @@
     1.4          val coind_witss =
     1.5            maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
     1.6  
     1.7 -        val _ = (warning o PolyML.makestring) (map length coind_wit_argsss)
     1.8 -        val _ = (warning o PolyML.makestring) (map length nonredundant_coind_wit_argsss)
     1.9 -
    1.10          fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
    1.11            let
    1.12              fun mk_goal sets y y_copy y'_copy j =