--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Mar 17 16:11:48 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Mar 17 16:26:08 2010 +0100
@@ -31,7 +31,8 @@
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
(* term -> bool *)
-fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], [])
+fun is_mono t =
+ Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], [])
fun is_const t =
let val T = fastype_of t in
is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),