src/HOL/Tools/SMT/smt_normalize.ML
changeset 40275 eed48b11abdb
parent 40274 6486c610a549
child 40278 0fc78bb54f18
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:05 2010 +0200
     1.3 @@ -69,11 +69,9 @@
     1.4        Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true
     1.5      | _ => false)
     1.6  
     1.7 -  val thms = map mk_meta_eq @{lemma
     1.8 -    "(case P of True => x | False => y) = (if P then x else y)"
     1.9 -    "(case P of False => y | True => x) = (if P then x else y)"
    1.10 -    by simp_all}
    1.11 -  val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
    1.12 +  val thm = mk_meta_eq @{lemma
    1.13 +    "(case P of True => x | False => y) = (if P then x else y)" by simp}
    1.14 +  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
    1.15  in
    1.16  fun rewrite_bool_cases ctxt =
    1.17    map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??