src/HOL/Tools/SMT/smt_translate.ML
changeset 39535 cd1bb7125d8a
parent 39483 9f0e5684f04b
child 40161 539d07b00e5f
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 17 20:53:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Sep 19 00:29:13 2010 +0200
     1.3 @@ -304,18 +304,19 @@
     1.4    let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
     1.5    in (Const (n, Us ---> T), sels) end
     1.6  
     1.7 -fun lookup_datatype ctxt n Ts = if n = @{type_name bool} then NONE else
     1.8 -  (case Datatype.get_info (ProofContext.theory_of ctxt) n of
     1.9 -    NONE => NONE  (* FIXME: also use Record.get_info *)
    1.10 -  | SOME {descr, ...} =>
    1.11 -      let
    1.12 -        val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
    1.13 -          (sort (int_ord o pairself fst) descr)
    1.14 -        val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
    1.15 -      in
    1.16 -        SOME (descr |> map (fn (i, (_, _, cs)) =>
    1.17 -          (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)))
    1.18 -      end)
    1.19 +fun lookup_datatype ctxt n Ts =
    1.20 +  if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE
    1.21 +  else
    1.22 +    Datatype.get_info (ProofContext.theory_of ctxt) n
    1.23 +    |> Option.map (fn {descr, ...} =>
    1.24 +         let
    1.25 +           val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
    1.26 +             (sort (int_ord o pairself fst) descr)
    1.27 +           val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
    1.28 +         in
    1.29 +           descr |> map (fn (i, (_, _, cs)) =>
    1.30 +             (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
    1.31 +         end)
    1.32  
    1.33  fun relaxed thms = (([], thms), map prop_of thms)
    1.34