fail for problems containg the universal sort (as those problems cannot be atomized)

--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Apr 07 19:48:58 2010 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Apr 07 20:38:11 2010 +0200
@@ -539,7 +539,8 @@
 
 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> (f (i1 := v1, i2 := v2)) i = f i" by smt
 
-lemma "(f g x = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)" by smt
+lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
+  by smt
 
 lemma "id 3 = 3 \<and> id True = True" by (smt id_def)
 

--- a/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 19:48:58 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 20:38:11 2010 +0200
@@ -262,11 +262,22 @@
            | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
 
   fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
+
+  val has_topsort = Term.exists_type (Term.exists_subtype (fn
+      TFree (_, []) => true
+    | TVar (_, []) => true
+    | _ => false))
 in
 fun smt_tac' pass_exns ctxt rules =
   Tactic.rtac @{thm ccontr} THEN'
   SUBPROOF (fn {context, prems, ...} =>
-    SAFE pass_exns (Tactic.rtac o smt_solver (rules @ prems)) context 1) ctxt
+    let val thms = rules @ prems
+    in
+      if exists (has_topsort o Thm.prop_of) thms
+      then fail_tac (trace_msg context I)
+        "SMT: proof state contains the universal sort {}"
+      else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1
+    end) ctxt
 
 val smt_tac = smt_tac' false
 end