1.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed Nov 25 12:29:37 2009 +0100
     1.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed Nov 25 12:30:54 2009 +0100
     1.3 @@ -234,14 +234,18 @@
     1.4    fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
     1.5  
     1.6    val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
     1.7 +  val uses_nat_int =
     1.8 +    Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
     1.9  in
    1.10  fun nat_as_int ctxt thms =
    1.11    let
    1.12 -    fun norm thm uses_nat =
    1.13 -      if not (uses_nat_type (Thm.prop_of thm)) then (thm, uses_nat)
    1.14 -      else (Conv.fconv_rule (conv ctxt) thm, true)
    1.15 -    val (thms', uses_nat) = fold_map norm thms false
    1.16 -  in if uses_nat then nat_embedding @ thms' else thms' end
    1.17 +    fun norm thm = thm
    1.18 +      |> uses_nat_type (Thm.prop_of thm) ? Conv.fconv_rule (conv ctxt)
    1.19 +    val thms' = map norm thms
    1.20 +  in
    1.21 +    if exists (uses_nat_int o Thm.prop_of) thms' then nat_embedding @ thms'
    1.22 +    else thms'
    1.23 +  end
    1.24  end
    1.25  
    1.26