# HG changeset patch
# User boehmes
# Date 1284848953 -7200
# Node ID cd1bb7125d8a7b15faa6046313d2ef15e0f310cb
# Parent  c798d4f1b6828554067900dad62e6167ad94b8b9
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)

diff -r c798d4f1b682 -r cd1bb7125d8a src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 20:53:50 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Sep 19 00:29:13 2010 +0200
@@ -304,18 +304,19 @@
   let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
   in (Const (n, Us ---> T), sels) end
 
-fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
-  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
-    NONE => NONE  (* FIXME: also use Record.get_info *)
-  | SOME {descr, ...} =>
-      let
-        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
-          (sort (int_ord o pairself fst) descr)
-        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
-      in
-        SOME (descr |> map (fn (i, (_, _, cs)) =>
-          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
-      end)
+fun lookup_datatype ctxt n Ts =
+  if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE
+  else
+    Datatype.get_info (ProofContext.theory_of ctxt) n
+    |> Option.map (fn {descr, ...} =>
+         let
+           val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
+             (sort (int_ord o pairself fst) descr)
+           val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
+         in
+           descr |> map (fn (i, (_, _, cs)) =>
+             (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
+         end)
 
 fun relaxed thms = (([], thms), map prop_of thms)