# HG changeset patch
# User boehmes
# Date 1273701230 -7200
# Node ID d8ea5bff3ca42bc4d1a627cb93bb955b7d12c1b9
# Parent  9407b8d0f6ad032749ab2469326726d71969a11f
merged addition of rules into one function

diff -r 9407b8d0f6ad -r d8ea5bff3ca4 src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:49 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed May 12 23:53:50 2010 +0200
@@ -296,15 +296,19 @@
   val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
   val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
 
+  val add_pair_rules =
+    exists (exists_pair_type o Thm.prop_of) ?? append pair_rules
+
+
   val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
+
   val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
   val exists_fun_upd = Term.exists_subterm is_fun_upd
+
+  val add_fun_upd_rules =
+    exists (exists_fun_upd o Thm.prop_of) ?? append fun_upd_rules
 in
-fun add_pair_rules _ =
-  exists (exists_pair_type o Thm.prop_of) ?? append pair_rules
-
-fun add_fun_upd_rules _ =
-  exists (exists_fun_upd o Thm.prop_of) ?? append fun_upd_rules
+val add_rules = add_pair_rules #> add_fun_upd_rules
 end
 
 
@@ -508,8 +512,7 @@
   |> trivial_distinct ctxt
   |> positive_numerals ctxt
   |> nat_as_int ctxt
-  |> add_pair_rules ctxt
-  |> add_fun_upd_rules ctxt
+  |> add_rules
   |> map (unfold_defs ctxt #> normalize_rule ctxt)
   |> lift_lambdas ctxt
   |> apsnd (explicit_application ctxt)