src/HOL/Tools/SMT/smt_translate.ML
changeset 40681 872b08416fb4
parent 40664 e023788a91a1
child 40697 c3979dd80a50
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 24 08:51:48 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 24 10:39:58 2010 +0100
     1.3 @@ -194,6 +194,10 @@
     1.4        | is_builtin_conn' (@{const_name False}, _) = false
     1.5        | is_builtin_conn' c = is_builtin_conn c
     1.6  
     1.7 +    fun is_builtin_pred' ctxt (@{const_name distinct}, _) [t] =
     1.8 +          is_builtin_distinct andalso can HOLogic.dest_list t
     1.9 +      | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
    1.10 +
    1.11      val propT = @{typ prop} and boolT = @{typ bool}
    1.12      val as_propT = (fn @{typ bool} => propT | T => T)
    1.13      fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
    1.14 @@ -213,7 +217,7 @@
    1.15          (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
    1.16            c $ in_form t1 $ in_term t2 $ in_term t3
    1.17        | (h as Const c, ts) =>
    1.18 -          if is_builtin_conn' (conn c) orelse is_builtin_pred ctxt (pred c)
    1.19 +          if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
    1.20            then wrap_in_if (in_form t)
    1.21            else Term.list_comb (h, map in_term ts)
    1.22        | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
    1.23 @@ -237,8 +241,9 @@
    1.24          (q as Const (qn, _), [Abs (n, T, t')]) =>
    1.25            if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
    1.26            else as_term (in_term t)
    1.27 -      | (Const (c as (@{const_name SMT.distinct}, T)), [t']) =>
    1.28 -          if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
    1.29 +      | (Const (c as (@{const_name distinct}, T)), [t']) =>
    1.30 +          if is_builtin_distinct andalso can HOLogic.dest_list t' then
    1.31 +            Const (pred c) $ in_list T in_term t'
    1.32            else as_term (in_term t)
    1.33        | (Const c, ts) =>
    1.34            if is_builtin_conn (conn c)
    1.35 @@ -381,10 +386,10 @@
    1.36        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    1.37            transT T ##>> trans t1 ##>> trans t2 #>>
    1.38            (fn ((U, u1), u2) => SLet (U, u1, u2))
    1.39 -      | (h as Const (c as (@{const_name SMT.distinct}, T)), [t1]) =>
    1.40 -          (case builtin_fun ctxt c (HOLogic.dest_list t1) of
    1.41 +      | (h as Const (c as (@{const_name distinct}, T)), ts) =>
    1.42 +          (case builtin_fun ctxt c ts of
    1.43              SOME (n, ts) => fold_map trans ts #>> app n
    1.44 -          | NONE => transs h T [t1])
    1.45 +          | NONE => transs h T ts)
    1.46        | (h as Const (c as (_, T)), ts) =>
    1.47            (case try HOLogic.dest_number t of
    1.48              SOME (T, i) =>