# HG changeset patch
# User blanchet
# Date 1291637905 -3600
# Node ID 8cacefe9851c084dddfccb1576aceadcb5f972f1
# Parent  902ad76994d54a7860e60079c0c847567f3098ea
tuning

diff -r 902ad76994d5 -r 8cacefe9851c src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:18:25 2010 +0100
@@ -12,7 +12,7 @@
 begin
 
 ML {*
-exception FAIL
+exception BUG
 
 val subst = []
 val defs = Nitpick_HOL.all_axioms_of @{context} subst |> #1
@@ -30,7 +30,6 @@
    skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    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_const t =
@@ -38,10 +37,10 @@
     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
                                @{const False}))
   end
-fun mono t = is_mono t orelse raise FAIL
-fun nonmono t = not (is_mono t) orelse raise FAIL
-fun const t = is_const t orelse raise FAIL
-fun nonconst t = not (is_const t) orelse raise FAIL
+fun mono t = is_mono t orelse raise BUG
+fun nonmono t = not (is_mono t) orelse raise BUG
+fun const t = is_const t orelse raise BUG
+fun nonconst t = not (is_const t) orelse raise BUG
 *}
 
 ML {* const @{term "A::('a\<Rightarrow>'b)"} *}