src/HOL/Tools/SMT/smt_translate.ML
changeset 40274 6486c610a549
parent 40161 539d07b00e5f
child 40579 98ebd2300823
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Oct 29 17:38:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Oct 29 18:17:04 2010 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4          (q as Const (qn, _), [Abs (n, T, t')]) =>
     1.5            if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
     1.6            else as_term (in_term t)
     1.7 -      | (Const (c as (@{const_name distinct}, T)), [t']) =>
     1.8 +      | (Const (c as (@{const_name SMT.distinct}, T)), [t']) =>
     1.9            if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
    1.10            else as_term (in_term t)
    1.11        | (Const c, ts) =>
    1.12 @@ -377,7 +377,7 @@
    1.13        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    1.14            transT T ##>> trans t1 ##>> trans t2 #>>
    1.15            (fn ((U, u1), u2) => SLet (U, u1, u2))
    1.16 -      | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
    1.17 +      | (h as Const (c as (@{const_name SMT.distinct}, T)), [t1]) =>
    1.18            (case builtin_fun ctxt c (HOLogic.dest_list t1) of
    1.19              SOME (n, ts) => fold_map trans ts #>> app n
    1.20            | NONE => transs h T [t1])