1.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 02 22:54:42 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 02 22:54:42 2013 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4    val monomorph_limit: int Config.T
     1.5    val monomorph_instances: int Config.T
     1.6    val infer_triggers: bool Config.T
     1.7 -  val drop_bad_facts: bool Config.T
     1.8    val filter_only_facts: bool Config.T
     1.9    val debug_files: string Config.T
    1.10  
    1.11 @@ -161,7 +160,6 @@
    1.12  val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    1.13  val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    1.14  val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
    1.15 -val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
    1.16  val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
    1.17  val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
    1.18  

     2.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Oct 02 22:54:42 2013 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Oct 02 22:54:42 2013 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4  
     2.5  signature SMT_NORMALIZE =
     2.6  sig
     2.7 +  val drop_fact_warning: Proof.context -> thm -> unit
     2.8    val atomize_conv: Proof.context -> conv
     2.9    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    2.10    val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic ->
    2.11 @@ -18,6 +19,10 @@
    2.12  structure SMT_Normalize: SMT_NORMALIZE =
    2.13  struct
    2.14  
    2.15 +fun drop_fact_warning ctxt =
    2.16 +  SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
    2.17 +    Display.string_of_thm ctxt)
    2.18 +
    2.19  
    2.20  (* general theorem normalizations *)
    2.21  
    2.22 @@ -329,16 +334,10 @@
    2.23    |> Drule.forall_intr_vars
    2.24    |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
    2.25  
    2.26 -fun drop_fact_warning ctxt =
    2.27 -  let val pre = prefix "Warning: dropping assumption: "
    2.28 -  in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end
    2.29 -
    2.30  fun gen_norm1_safe ctxt (i, (weight, thm)) =
    2.31 -  if Config.get ctxt SMT_Config.drop_bad_facts then
    2.32 -    (case try (gen_normalize1 ctxt weight) thm of
    2.33 -      SOME thm' => SOME (i, thm')
    2.34 -    | NONE => (drop_fact_warning ctxt thm; NONE))
    2.35 -  else SOME (i, gen_normalize1 ctxt weight thm)
    2.36 +  (case try (gen_normalize1 ctxt weight) thm of
    2.37 +    SOME thm' => SOME (i, thm')
    2.38 +  | NONE => (drop_fact_warning ctxt thm; NONE))
    2.39  
    2.40  fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
    2.41  

     3.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Oct 02 22:54:42 2013 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Oct 02 22:54:42 2013 +0200
     3.3 @@ -257,11 +257,13 @@
     3.4    | _ => false))
     3.5  
     3.6  (* without this test, we would run into problems when atomizing the rules: *)
     3.7 -fun check_topsort iwthms =
     3.8 -  if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then
     3.9 -    raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
    3.10 -      "contains the universal sort {}"))
    3.11 -  else ()
    3.12 +fun check_topsort ctxt thm =
    3.13 +  if has_topsort (Thm.prop_of thm) then
    3.14 +    (SMT_Normalize.drop_fact_warning ctxt thm; TrueI)
    3.15 +  else
    3.16 +    thm
    3.17 +
    3.18 +fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms
    3.19  
    3.20  
    3.21  (* filter *)
    3.22 @@ -277,7 +279,6 @@
    3.23      val ctxt =
    3.24        ctxt
    3.25        |> Config.put SMT_Config.oracle false
    3.26 -      |> Config.put SMT_Config.drop_bad_facts true
    3.27        |> Config.put SMT_Config.filter_only_facts true
    3.28  
    3.29      val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
    3.30 @@ -291,7 +292,7 @@
    3.31      map snd xwthms
    3.32      |> map_index I
    3.33      |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
    3.34 -    |> tap check_topsort
    3.35 +    |> check_topsorts ctxt'
    3.36      |> gen_preprocess ctxt'
    3.37      |> pair (map (apsnd snd) xwthms)
    3.38    end
    3.39 @@ -332,7 +333,7 @@
    3.40  
    3.41    fun solve ctxt iwthms =
    3.42      iwthms
    3.43 -    |> tap check_topsort
    3.44 +    |> check_topsorts ctxt
    3.45      |> apply_solver ctxt
    3.46      |>> trace_assumptions ctxt iwthms
    3.47      |> snd