merged

--- a/src/HOL/Inductive.thy	Fri Nov 27 08:42:50 2009 +0100
+++ b/src/HOL/Inductive.thy	Mon Nov 30 08:08:31 2009 +0100
@@ -261,18 +261,13 @@
 theorems basic_monos =
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   Collect_mono in_mono vimage_mono
-  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
-  not_all not_ex
-  Ball_def Bex_def
-  induct_rulify_fallback
 
 use "Tools/inductive.ML"
 setup Inductive.setup
 
 theorems [mono] =
   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
-  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
-  not_all not_ex
+  imp_mono not_mono
   Ball_def Bex_def
   induct_rulify_fallback
 

--- a/src/HOL/Tools/inductive.ML	Fri Nov 27 08:42:50 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Nov 30 08:08:31 2009 +0100
@@ -177,26 +177,22 @@
 
 fun mk_mono thm =
   let
-    val concl = concl_of thm;
-    fun eq2mono thm' = [thm' RS (thm' RS eq_to_mono)] @
-      (case concl of
-          (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
-        | _ => [thm' RS (thm' RS eq_to_mono2)]);
+    fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
     fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
       handle THM _ => thm RS @{thm le_boolD}
   in
-    case concl of
+    case concl_of thm of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
     | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
-      [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
-         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
-    | _ => [thm]
+      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
+        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
+    | _ => thm
   end handle THM _ =>
     error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
 
-val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
-val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
+val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono);
+val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono);
 
 
 
@@ -338,7 +334,7 @@
       REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST
         [atac 1,
-         resolve_tac (maps mk_mono monos @ get_monos ctxt) 1,
+         resolve_tac (map mk_mono monos @ get_monos ctxt) 1,
          etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));