src/HOL/Tools/SMT/smt_normalize.ML
changeset 54041 227908156cd2
parent 51717 9e7d1c139569
child 54293 cd896760fa0f
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Oct 02 22:54:42 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Oct 02 22:54:42 2013 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature SMT_NORMALIZE =
     1.6  sig
     1.7 +  val drop_fact_warning: Proof.context -> thm -> unit
     1.8    val atomize_conv: Proof.context -> conv
     1.9    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    1.10    val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic ->
    1.11 @@ -18,6 +19,10 @@
    1.12  structure SMT_Normalize: SMT_NORMALIZE =
    1.13  struct
    1.14  
    1.15 +fun drop_fact_warning ctxt =
    1.16 +  SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
    1.17 +    Display.string_of_thm ctxt)
    1.18 +
    1.19  
    1.20  (* general theorem normalizations *)
    1.21  
    1.22 @@ -329,16 +334,10 @@
    1.23    |> Drule.forall_intr_vars
    1.24    |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
    1.25  
    1.26 -fun drop_fact_warning ctxt =
    1.27 -  let val pre = prefix "Warning: dropping assumption: "
    1.28 -  in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end
    1.29 -
    1.30  fun gen_norm1_safe ctxt (i, (weight, thm)) =
    1.31 -  if Config.get ctxt SMT_Config.drop_bad_facts then
    1.32 -    (case try (gen_normalize1 ctxt weight) thm of
    1.33 -      SOME thm' => SOME (i, thm')
    1.34 -    | NONE => (drop_fact_warning ctxt thm; NONE))
    1.35 -  else SOME (i, gen_normalize1 ctxt weight thm)
    1.36 +  (case try (gen_normalize1 ctxt weight) thm of
    1.37 +    SOME thm' => SOME (i, thm')
    1.38 +  | NONE => (drop_fact_warning ctxt thm; NONE))
    1.39  
    1.40  fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
    1.41