make SMT integration slacker w.r.t. bad apples (facts)

--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 02 22:54:42 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 02 22:54:42 2013 +0200
@@ -33,7 +33,6 @@
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
   val infer_triggers: bool Config.T
-  val drop_bad_facts: bool Config.T
   val filter_only_facts: bool Config.T
   val debug_files: string Config.T
 
@@ -161,7 +160,6 @@
 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
 val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
-val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
 val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
 val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
 

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Oct 02 22:54:42 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Oct 02 22:54:42 2013 +0200
@@ -6,6 +6,7 @@
 
 signature SMT_NORMALIZE =
 sig
+  val drop_fact_warning: Proof.context -> thm -> unit
   val atomize_conv: Proof.context -> conv
   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic ->
@@ -18,6 +19,10 @@
 structure SMT_Normalize: SMT_NORMALIZE =
 struct
 
+fun drop_fact_warning ctxt =
+  SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
+    Display.string_of_thm ctxt)
+
 
 (* general theorem normalizations *)
 
@@ -329,16 +334,10 @@
   |> Drule.forall_intr_vars
   |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
 
-fun drop_fact_warning ctxt =
-  let val pre = prefix "Warning: dropping assumption: "
-  in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end
-
 fun gen_norm1_safe ctxt (i, (weight, thm)) =
-  if Config.get ctxt SMT_Config.drop_bad_facts then
-    (case try (gen_normalize1 ctxt weight) thm of
-      SOME thm' => SOME (i, thm')
-    | NONE => (drop_fact_warning ctxt thm; NONE))
-  else SOME (i, gen_normalize1 ctxt weight thm)
+  (case try (gen_normalize1 ctxt weight) thm of
+    SOME thm' => SOME (i, thm')
+  | NONE => (drop_fact_warning ctxt thm; NONE))
 
 fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
 

--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Oct 02 22:54:42 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Oct 02 22:54:42 2013 +0200
@@ -257,11 +257,13 @@
   | _ => false))
 
 (* without this test, we would run into problems when atomizing the rules: *)
-fun check_topsort iwthms =
-  if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then
-    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
-      "contains the universal sort {}"))
-  else ()
+fun check_topsort ctxt thm =
+  if has_topsort (Thm.prop_of thm) then
+    (SMT_Normalize.drop_fact_warning ctxt thm; TrueI)
+  else
+    thm
+
+fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms
 
 
 (* filter *)
@@ -277,7 +279,6 @@
     val ctxt =
       ctxt
       |> Config.put SMT_Config.oracle false
-      |> Config.put SMT_Config.drop_bad_facts true
       |> Config.put SMT_Config.filter_only_facts true
 
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
@@ -291,7 +292,7 @@
     map snd xwthms
     |> map_index I
     |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
-    |> tap check_topsort
+    |> check_topsorts ctxt'
     |> gen_preprocess ctxt'
     |> pair (map (apsnd snd) xwthms)
   end
@@ -332,7 +333,7 @@
 
   fun solve ctxt iwthms =
     iwthms
-    |> tap check_topsort
+    |> check_topsorts ctxt
     |> apply_solver ctxt
     |>> trace_assumptions ctxt iwthms
     |> snd