# HG changeset patch
# User boehmes
# Date 1259148654 -3600
# Node ID 3e7c51bbeb246b8458a1831344aa03124656d6ec
# Parent  395df8f652b6538d670bda08cfdea0e35f6f1e5b
only add nat/int conversion rules if necessary

diff -r 395df8f652b6 -r 3e7c51bbeb24 src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed Nov 25 12:29:37 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed Nov 25 12:30:54 2009 +0100
@@ -234,14 +234,18 @@
   fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
 
   val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
+  val uses_nat_int =
+    Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
 in
 fun nat_as_int ctxt thms =
   let
-    fun norm thm uses_nat =
-      if not (uses_nat_type (Thm.prop_of thm)) then (thm, uses_nat)
-      else (Conv.fconv_rule (conv ctxt) thm, true)
-    val (thms', uses_nat) = fold_map norm thms false
-  in if uses_nat then nat_embedding @ thms' else thms' end
+    fun norm thm = thm
+      |> uses_nat_type (Thm.prop_of thm) ? Conv.fconv_rule (conv ctxt)
+    val thms' = map norm thms
+  in
+    if exists (uses_nat_int o Thm.prop_of) thms' then nat_embedding @ thms'
+    else thms'
+  end
 end