diff -r 8e2f2398aae7 -r e58d1cdda832 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:56:56 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:56:56 2010 +0100
@@ -67,7 +67,6 @@
 ML {* Nitpick_Mono.trace := false *}
 
 ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
-(*
 ML {* const @{term "(A\<Colon>'a set) = A"} *}
 ML {* const @{term "(A\<Colon>'a set set) = A"} *}
 ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
@@ -138,7 +137,6 @@
 
 ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
 ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
-*)
 
 ML {*
 val preproc_timeout = SOME (seconds 5.0)
@@ -184,8 +182,6 @@
 
 fun check_theory thy =
   let
-    val finitizes = [(NONE, SOME false)]
-    val monos = [(NONE, SOME false)]
     val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
     val _ = File.write path ""
     fun check_theorem (name, th) =
@@ -193,8 +189,7 @@
         val t = th |> prop_of |> Type.legacy_freeze |> close_form
         val neg_t = Logic.mk_implies (t, @{prop False})
         val (nondef_ts, def_ts, _, _, _) =
-          time_limit preproc_timeout
-              (preprocess_formulas hol_ctxt finitizes monos []) neg_t
+          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
       in File.append path (res ^ "\n"); writeln res end
       handle TimeLimit.TimeOut => ()