fixed trigger inference: testing if a theorem already has a trigger was too strict;
fixed monomorphization with respect to triggers (which might occur schematically)

--- a/src/HOL/SMT.thy	Wed Dec 15 16:32:45 2010 +0100
+++ b/src/HOL/SMT.thy	Wed Dec 15 18:18:56 2010 +0100
@@ -11,7 +11,7 @@
   "Tools/SMT/smt_utils.ML"
   "Tools/SMT/smt_failure.ML"
   "Tools/SMT/smt_config.ML"
-  "Tools/SMT/smt_monomorph.ML"
+  ("Tools/SMT/smt_monomorph.ML")
   ("Tools/SMT/smt_builtin.ML")
   ("Tools/SMT/smt_normalize.ML")
   ("Tools/SMT/smt_translate.ML")
@@ -149,6 +149,7 @@
 
 subsection {* Setup *}
 
+use "Tools/SMT/smt_monomorph.ML"
 use "Tools/SMT/smt_builtin.ML"
 use "Tools/SMT/smt_normalize.ML"
 use "Tools/SMT/smt_translate.ML"

--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Dec 15 16:32:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Dec 15 18:18:56 2010 +0100
@@ -45,8 +45,19 @@
 fun is_const pred (n, T) = not (ignored n) andalso pred T
 
 fun collect_consts_if pred f =
-  Thm.prop_of #>
-  Term.fold_aterms (fn Const c => if is_const pred c then f c else I | _ => I)
+  let
+    fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
+      | collect (t $ u) = collect t #> collect u
+      | collect (Abs (_, _, t)) = collect t
+      | collect (Const c) = if is_const pred c then f c else I
+      | collect _ = I
+    and collect_trigger t =
+      let val dest = these o try HOLogic.dest_list 
+      in fold (fold collect_pat o dest) (dest t) end
+    and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
+      | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
+      | collect_pat _ = I
+  in collect o Thm.prop_of end
 
 val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
 

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 16:32:45 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 18:18:56 2010 +0100
@@ -183,7 +183,7 @@
           (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
             ([], []) => [[ct]]
           | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
-      | _ => [[ct]])
+      | _ => [])
     else []
 
   fun proper_mpat _ _ _ [] = false
@@ -227,8 +227,11 @@
 
     in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
 
+  fun has_trigger (@{const SMT.trigger} $ _ $ _) = true
+    | has_trigger _ = false
+
   fun try_trigger_conv cv ct =
-    if proper_quant false (K false) (Thm.term_of ct) then Conv.all_conv ct
+    if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
     else Conv.try_conv cv ct
 
   fun infer_trigger_conv ctxt =