# HG changeset patch
# User boehmes
# Date 1288369025 -7200
# Node ID eed48b11abdb5cf15a851e36b1db841e126ff42b
# Parent  6486c610a54909560f5f13e979ba4846dd3bc966
tuned

diff -r 6486c610a549 -r eed48b11abdb src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:04 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:05 2010 +0200
@@ -69,11 +69,9 @@
       Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true
     | _ => false)
 
-  val thms = map mk_meta_eq @{lemma
-    "(case P of True => x | False => y) = (if P then x else y)"
-    "(case P of False => y | True => x) = (if P then x else y)"
-    by simp_all}
-  val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
+  val thm = mk_meta_eq @{lemma
+    "(case P of True => x | False => y) = (if P then x else y)" by simp}
+  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
 in
 fun rewrite_bool_cases ctxt =
   map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??