1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Nov 24 08:51:48 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Nov 24 10:39:58 2010 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4              | NONE => NONE)
     1.5          | is_unique _ = NONE
     1.6        fun mk_unique_axiom T ts =
     1.7 -        Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
     1.8 +        Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
     1.9            HOLogic.mk_list T ts
    1.10      in
    1.11        map_filter is_unique fns
    1.12 @@ -383,7 +383,7 @@
    1.13    fun mk_list T = HOLogic.mk_list T
    1.14  
    1.15    fun mk_distinct T ts =
    1.16 -    Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
    1.17 +    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
    1.18        mk_list T ts
    1.19  
    1.20    fun quant name f = scan_line name (num -- num -- num) >> pair f

     2.1 --- a/src/HOL/SMT.thy	Wed Nov 24 08:51:48 2010 +0100
     2.2 +++ b/src/HOL/SMT.thy	Wed Nov 24 10:39:58 2010 +0100
     2.3 @@ -81,20 +81,6 @@
     2.4  
     2.5  
     2.6  
     2.7 -subsection {* Distinctness *}
     2.8 -
     2.9 -text {*
    2.10 -As an abbreviation for a quadratic number of inequalities, SMT solvers
    2.11 -provide a built-in @{text distinct}.  To avoid confusion with the
    2.12 -already defined (and more general) @{term List.distinct}, a separate
    2.13 -constant is defined.
    2.14 -*}
    2.15 -
    2.16 -definition distinct :: "'a list \<Rightarrow> bool"
    2.17 -where "distinct xs = List.distinct xs"
    2.18 -
    2.19 -
    2.20 -
    2.21  subsection {* Higher-order encoding *}
    2.22  
    2.23  text {*
    2.24 @@ -369,7 +355,7 @@
    2.25  
    2.26  hide_type (open) pattern
    2.27  hide_const Pattern term_eq
    2.28 -hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
    2.29 +hide_const (open) trigger pat nopat weight fun_app z3div z3mod
    2.30  
    2.31  
    2.32  

     3.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Wed Nov 24 08:51:48 2010 +0100
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Wed Nov 24 10:39:58 2010 +0100
     3.3 @@ -16193,3 +16193,101 @@
     3.4  #223 := [asserted]: #31
     3.5  [unit-resolution #223 #592]: false
     3.6  unsat
     3.7 +030f06ff279b2b609c311e25ffea5c845380fd2c 97 0
     3.8 +#2 := false
     3.9 +decl f1 :: S1
    3.10 +#4 := f1
    3.11 +decl f2 :: S1
    3.12 +#5 := f2
    3.13 +#9 := 3::int
    3.14 +decl f3 :: int
    3.15 +#8 := f3
    3.16 +#46 := (>= f3 3::int)
    3.17 +#51 := (ite #46 f2 f1)
    3.18 +#73 := (= f1 #51)
    3.19 +#58 := (ite #46 f1 f2)
    3.20 +#69 := (= f1 #58)
    3.21 +#115 := (iff #69 #73)
    3.22 +#113 := (iff #73 #69)
    3.23 +#61 := (= #51 #58)
    3.24 +#12 := (<= 3::int f3)
    3.25 +#13 := (ite #12 f1 f2)
    3.26 +#10 := (< f3 3::int)
    3.27 +#11 := (ite #10 f1 f2)
    3.28 +#14 := (distinct #11 #13)
    3.29 +#15 := (not #14)
    3.30 +#64 := (iff #15 #61)
    3.31 +#33 := (= #11 #13)
    3.32 +#62 := (iff #33 #61)
    3.33 +#59 := (= #13 #58)
    3.34 +#56 := (iff #12 #46)
    3.35 +#57 := [rewrite]: #56
    3.36 +#60 := [monotonicity #57]: #59
    3.37 +#54 := (= #11 #51)
    3.38 +#44 := (not #46)
    3.39 +#48 := (ite #44 f1 f2)
    3.40 +#52 := (= #48 #51)
    3.41 +#53 := [rewrite]: #52
    3.42 +#49 := (= #11 #48)
    3.43 +#45 := (iff #10 #44)
    3.44 +#47 := [rewrite]: #45
    3.45 +#50 := [monotonicity #47]: #49
    3.46 +#55 := [trans #50 #53]: #54
    3.47 +#63 := [monotonicity #55 #60]: #62
    3.48 +#42 := (iff #15 #33)
    3.49 +#34 := (not #33)
    3.50 +#37 := (not #34)
    3.51 +#40 := (iff #37 #33)
    3.52 +#41 := [rewrite]: #40
    3.53 +#38 := (iff #15 #37)
    3.54 +#35 := (iff #14 #34)
    3.55 +#36 := [rewrite]: #35
    3.56 +#39 := [monotonicity #36]: #38
    3.57 +#43 := [trans #39 #41]: #42
    3.58 +#65 := [trans #43 #63]: #64
    3.59 +#32 := [asserted]: #15
    3.60 +#66 := [mp #32 #65]: #61
    3.61 +#114 := [monotonicity #66]: #113
    3.62 +#116 := [symm #114]: #115
    3.63 +#109 := (not #73)
    3.64 +#6 := (= f1 f2)
    3.65 +#67 := (= f2 #58)
    3.66 +#105 := (iff #67 #6)
    3.67 +#103 := (iff #6 #67)
    3.68 +#98 := (= #58 f2)
    3.69 +#101 := (iff #98 #67)
    3.70 +#102 := [commutativity]: #101
    3.71 +#99 := (iff #6 #98)
    3.72 +#96 := [hypothesis]: #73
    3.73 +#97 := [trans #96 #66]: #69
    3.74 +#100 := [monotonicity #97]: #99
    3.75 +#104 := [trans #100 #102]: #103
    3.76 +#106 := [symm #104]: #105
    3.77 +#72 := (= f2 #51)
    3.78 +#84 := (iff #72 #67)
    3.79 +#85 := [monotonicity #66]: #84
    3.80 +#80 := (not #67)
    3.81 +#81 := [hypothesis]: #80
    3.82 +#78 := (or #46 #67)
    3.83 +#79 := [def-axiom]: #78
    3.84 +#82 := [unit-resolution #79 #81]: #46
    3.85 +#74 := (or #44 #72)
    3.86 +#75 := [def-axiom]: #74
    3.87 +#83 := [unit-resolution #75 #82]: #72
    3.88 +#86 := [mp #83 #85]: #67
    3.89 +#87 := [unit-resolution #81 #86]: false
    3.90 +#88 := [lemma #87]: #67
    3.91 +#107 := [mp #88 #106]: #6
    3.92 +#7 := (not #6)
    3.93 +#31 := [asserted]: #7
    3.94 +#108 := [unit-resolution #31 #107]: false
    3.95 +#110 := [lemma #108]: #109
    3.96 +#70 := (or #46 #73)
    3.97 +#71 := [def-axiom]: #70
    3.98 +#111 := [unit-resolution #71 #110]: #46
    3.99 +#76 := (or #44 #69)
   3.100 +#77 := [def-axiom]: #76
   3.101 +#112 := [unit-resolution #77 #111]: #69
   3.102 +#117 := [mp #112 #116]: #73
   3.103 +[unit-resolution #110 #117]: false
   3.104 +unsat

     4.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Wed Nov 24 08:51:48 2010 +0100
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Wed Nov 24 10:39:58 2010 +0100
     4.3 @@ -293,11 +293,11 @@
     4.4  
     4.5  lemma "(0 \<le> y + -1 * x \<or> \<not> 0 \<le> x \<or> 0 \<le> (x::int)) = (\<not> False)" by smt
     4.6  
     4.7 -lemma "SMT.distinct [x < (3::int), 3 \<le> x]" by smt
     4.8 +lemma "distinct [x < (3::int), 3 \<le> x]" by smt
     4.9  
    4.10  lemma
    4.11    assumes "a > (0::int)"
    4.12 -  shows "SMT.distinct [a, a * 2, a - a]"
    4.13 +  shows "distinct [a, a * 2, a - a]"
    4.14    using assms by smt
    4.15  
    4.16  lemma "
    4.17 @@ -430,7 +430,7 @@
    4.18     False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
    4.19    by smt
    4.20  
    4.21 -lemma "SMT.distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
    4.22 +lemma "distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
    4.23  
    4.24  lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
    4.25  

     5.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Nov 24 08:51:48 2010 +0100
     5.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Wed Nov 24 10:39:58 2010 +0100
     5.3 @@ -53701,3 +53701,42 @@
     5.4  #60 := [asserted]: #10
     5.5  [mp #60 #69]: false
     5.6  unsat
     5.7 +c4d2e4408924ee75f6b9b17e513fd22b6307bf65 38 0
     5.8 +#2 := false
     5.9 +decl f4 :: S2
    5.10 +#9 := f4
    5.11 +decl f3 :: S2
    5.12 +#8 := f3
    5.13 +#11 := (distinct f3 f4)
    5.14 +#12 := (not #11)
    5.15 +#10 := (= f3 f4)
    5.16 +#13 := (implies #10 #12)
    5.17 +#14 := (not #13)
    5.18 +#54 := (iff #14 false)
    5.19 +#1 := true
    5.20 +#49 := (not true)
    5.21 +#52 := (iff #49 false)
    5.22 +#53 := [rewrite]: #52
    5.23 +#50 := (iff #14 #49)
    5.24 +#47 := (iff #13 true)
    5.25 +#42 := (implies #10 #10)
    5.26 +#45 := (iff #42 true)
    5.27 +#46 := [rewrite]: #45
    5.28 +#43 := (iff #13 #42)
    5.29 +#40 := (iff #12 #10)
    5.30 +#32 := (not #10)
    5.31 +#35 := (not #32)
    5.32 +#38 := (iff #35 #10)
    5.33 +#39 := [rewrite]: #38
    5.34 +#36 := (iff #12 #35)
    5.35 +#33 := (iff #11 #32)
    5.36 +#34 := [rewrite]: #33
    5.37 +#37 := [monotonicity #34]: #36
    5.38 +#41 := [trans #37 #39]: #40
    5.39 +#44 := [monotonicity #41]: #43
    5.40 +#48 := [trans #44 #46]: #47
    5.41 +#51 := [monotonicity #48]: #50
    5.42 +#55 := [trans #51 #53]: #54
    5.43 +#31 := [asserted]: #14
    5.44 +[mp #31 #55]: false
    5.45 +unsat

     6.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Nov 24 08:51:48 2010 +0100
     6.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Nov 24 10:39:58 2010 +0100
     6.3 @@ -104,15 +104,15 @@
     6.4    by smt+
     6.5  
     6.6  lemma
     6.7 -  "SMT.distinct []"
     6.8 -  "SMT.distinct [a]"
     6.9 -  "SMT.distinct [a, b, c] \<longrightarrow> a \<noteq> c"
    6.10 -  "SMT.distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d"
    6.11 -  "\<not> SMT.distinct [a, b, a, b]"
    6.12 -  "a = b \<longrightarrow> \<not> SMT.distinct [a, b]"
    6.13 -  "a = b \<and> a = c \<longrightarrow> \<not> SMT.distinct [a, b, c]"
    6.14 -  "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [d, b, c, a]"
    6.15 -  "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [a, b, c] \<and> SMT.distinct [b, c, d]"
    6.16 +  "distinct []"
    6.17 +  "distinct [a]"
    6.18 +  "distinct [a, b, c] \<longrightarrow> a \<noteq> c"
    6.19 +  "distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d"
    6.20 +  "\<not> distinct [a, b, a, b]"
    6.21 +  "a = b \<longrightarrow> \<not> distinct [a, b]"
    6.22 +  "a = b \<and> a = c \<longrightarrow> \<not> distinct [a, b, c]"
    6.23 +  "distinct [a, b, c, d] \<longrightarrow> distinct [d, b, c, a]"
    6.24 +  "distinct [a, b, c, d] \<longrightarrow> distinct [a, b, c] \<and> distinct [b, c, d]"
    6.25    by smt+
    6.26  
    6.27  lemma
    6.28 @@ -193,7 +193,7 @@
    6.29    by smt+
    6.30  
    6.31  lemma
    6.32 -  "SMT.distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
    6.33 +  "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
    6.34    sorry  (* FIXME: injective function *)
    6.35  
    6.36  lemma
    6.37 @@ -636,7 +636,7 @@
    6.38    "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2"
    6.39    "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
    6.40    "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
    6.41 -  "SMT.distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
    6.42 +  "distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
    6.43    by smt+
    6.44  
    6.45  

     7.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 08:51:48 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 10:39:58 2010 +0100
     7.3 @@ -53,7 +53,8 @@
     7.4    (@{const_name If}, K true),
     7.5    (@{const_name bool.bool_case}, K true),
     7.6    (@{const_name Let}, K true),
     7.7 -  (@{const_name SMT.distinct}, K true),
     7.8 +  (* (@{const_name distinct}, K true),  -- not a real builtin, only when
     7.9 +                                           applied to an explicit list *)
    7.10  
    7.11    (* technicalities *)
    7.12    (@{const_name SMT.pat}, K true),

     8.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 08:51:48 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 10:39:58 2010 +0100
     8.3 @@ -39,18 +39,18 @@
     8.4     three elements in the argument list) *)
     8.5  
     8.6  local
     8.7 -  fun is_trivial_distinct (Const (@{const_name SMT.distinct}, _) $ t) =
     8.8 -       (length (HOLogic.dest_list t) <= 2
     8.9 -        handle TERM _ => error ("SMT: constant " ^
    8.10 -          quote @{const_name SMT.distinct} ^ " must be applied to " ^
    8.11 -          "an explicit list."))
    8.12 +  fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
    8.13 +        (case try HOLogic.dest_list t of
    8.14 +          SOME [] => true
    8.15 +        | SOME [_] => true
    8.16 +        | _ => false)
    8.17      | is_trivial_distinct _ = false
    8.18  
    8.19    val thms = map mk_meta_eq @{lemma
    8.20 -    "SMT.distinct [] = True"
    8.21 -    "SMT.distinct [x] = True"
    8.22 -    "SMT.distinct [x, y] = (x ~= y)"
    8.23 -    by (simp_all add: distinct_def)}
    8.24 +    "distinct [] = True"
    8.25 +    "distinct [x] = True"
    8.26 +    "distinct [x, y] = (x ~= y)"
    8.27 +    by simp_all}
    8.28    fun distinct_conv _ =
    8.29      U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    8.30  in

     9.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 24 08:51:48 2010 +0100
     9.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 24 10:39:58 2010 +0100
     9.3 @@ -194,6 +194,10 @@
     9.4        | is_builtin_conn' (@{const_name False}, _) = false
     9.5        | is_builtin_conn' c = is_builtin_conn c
     9.6  
     9.7 +    fun is_builtin_pred' ctxt (@{const_name distinct}, _) [t] =
     9.8 +          is_builtin_distinct andalso can HOLogic.dest_list t
     9.9 +      | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
    9.10 +
    9.11      val propT = @{typ prop} and boolT = @{typ bool}
    9.12      val as_propT = (fn @{typ bool} => propT | T => T)
    9.13      fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
    9.14 @@ -213,7 +217,7 @@
    9.15          (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
    9.16            c $ in_form t1 $ in_term t2 $ in_term t3
    9.17        | (h as Const c, ts) =>
    9.18 -          if is_builtin_conn' (conn c) orelse is_builtin_pred ctxt (pred c)
    9.19 +          if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
    9.20            then wrap_in_if (in_form t)
    9.21            else Term.list_comb (h, map in_term ts)
    9.22        | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
    9.23 @@ -237,8 +241,9 @@
    9.24          (q as Const (qn, _), [Abs (n, T, t')]) =>
    9.25            if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
    9.26            else as_term (in_term t)
    9.27 -      | (Const (c as (@{const_name SMT.distinct}, T)), [t']) =>
    9.28 -          if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
    9.29 +      | (Const (c as (@{const_name distinct}, T)), [t']) =>
    9.30 +          if is_builtin_distinct andalso can HOLogic.dest_list t' then
    9.31 +            Const (pred c) $ in_list T in_term t'
    9.32            else as_term (in_term t)
    9.33        | (Const c, ts) =>
    9.34            if is_builtin_conn (conn c)
    9.35 @@ -381,10 +386,10 @@
    9.36        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    9.37            transT T ##>> trans t1 ##>> trans t2 #>>
    9.38            (fn ((U, u1), u2) => SLet (U, u1, u2))
    9.39 -      | (h as Const (c as (@{const_name SMT.distinct}, T)), [t1]) =>
    9.40 -          (case builtin_fun ctxt c (HOLogic.dest_list t1) of
    9.41 +      | (h as Const (c as (@{const_name distinct}, T)), ts) =>
    9.42 +          (case builtin_fun ctxt c ts of
    9.43              SOME (n, ts) => fold_map trans ts #>> app n
    9.44 -          | NONE => transs h T [t1])
    9.45 +          | NONE => transs h T ts)
    9.46        | (h as Const (c as (_, T)), ts) =>
    9.47            (case try HOLogic.dest_number t of
    9.48              SOME (T, i) =>

    10.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Nov 24 08:51:48 2010 +0100
    10.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Nov 24 10:39:58 2010 +0100
    10.3 @@ -167,8 +167,11 @@
    10.4    | conn @{const_name If} = SOME "if_then_else"
    10.5    | conn _ = NONE
    10.6  
    10.7 -fun pred @{const_name SMT.distinct} _ = SOME "distinct"
    10.8 -  | pred @{const_name HOL.eq} _ = SOME "="
    10.9 +fun distinct_pred (@{const_name distinct}, _) [t] =
   10.10 +      try HOLogic.dest_list t |> Option.map (pair "distinct")
   10.11 +  | distinct_pred _ _ = NONE
   10.12 +
   10.13 +fun pred @{const_name HOL.eq} _ = SOME "="
   10.14    | pred @{const_name term_eq} _ = SOME "="
   10.15    | pred @{const_name less} T = if_int_type T "<"
   10.16    | pred @{const_name less_eq} T = if_int_type T "<="
   10.17 @@ -192,7 +195,10 @@
   10.18  fun builtin_fun ctxt (c as (n, T)) ts =
   10.19    let
   10.20      val builtin_func' = chained_builtin_func (get_builtins ctxt)
   10.21 -    val builtin_pred' = chained_builtin_pred (get_builtins ctxt)
   10.22 +    fun builtin_pred' c t =
   10.23 +      (case distinct_pred c ts of
   10.24 +        SOME b => SOME b
   10.25 +      | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
   10.26    in
   10.27      if is_connT T then conn n |> Option.map (rpair ts)
   10.28      else if is_predT T then

    11.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Nov 24 08:51:48 2010 +0100
    11.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Nov 24 10:39:58 2010 +0100
    11.3 @@ -182,7 +182,7 @@
    11.4  fun mk_list cT cts =
    11.5    fold_rev (Thm.mk_binop (U.instT cT cons_term)) cts (U.instT cT nil_term)
    11.6  
    11.7 -val distinct = U.mk_const_pat @{theory} @{const_name SMT.distinct}
    11.8 +val distinct = U.mk_const_pat @{theory} @{const_name distinct}
    11.9    (U.destT1 o U.destT1)
   11.10  fun mk_distinct [] = mk_true
   11.11    | mk_distinct (cts as (ct :: _)) =

    12.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Nov 24 08:51:48 2010 +0100
    12.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Nov 24 10:39:58 2010 +0100
    12.3 @@ -308,14 +308,14 @@
    12.4            prove disjI3 (L.negate ct2, false) (ct1, false)
    12.5        | @{const HOL.disj} $ _ $ _ =>
    12.6            prove disjI2 (L.negate ct1, false) (ct2, true)
    12.7 -      | Const (@{const_name SMT.distinct}, _) $ _ =>
    12.8 +      | Const (@{const_name distinct}, _) $ _ =>
    12.9            let
   12.10              fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
   12.11              fun prv cu =
   12.12                let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
   12.13                in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
   12.14            in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
   12.15 -      | @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
   12.16 +      | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
   12.17            let
   12.18              fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
   12.19              fun prv cu =
   12.20 @@ -481,7 +481,7 @@
   12.21      (case Term.head_of (Thm.term_of cl) of
   12.22        @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
   12.23      | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
   12.24 -    | Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
   12.25 +    | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
   12.26      | _ => prove (prove_eq_safe f)) cp
   12.27  in
   12.28  fun monotonicity eqs ct =

    13.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Nov 24 08:51:48 2010 +0100
    13.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Nov 24 10:39:58 2010 +0100
    13.3 @@ -197,7 +197,7 @@
    13.4        | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
    13.5        | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
    13.6        | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
    13.7 -      | Const (@{const_name SMT.distinct}, _) $ _ =>
    13.8 +      | Const (@{const_name distinct}, _) $ _ =>
    13.9            if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
   13.10            else fresh_abstraction cvs ct
   13.11        | Const (@{const_name If}, _) $ _ $ _ $ _ =>
   13.12 @@ -258,9 +258,9 @@
   13.13      (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
   13.14      (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
   13.15  
   13.16 -  val dist1 = @{lemma "SMT.distinct [] == ~False" by (simp add: distinct_def)}
   13.17 -  val dist2 = @{lemma "SMT.distinct [x] == ~False" by (simp add: distinct_def)}
   13.18 -  val dist3 = @{lemma "SMT.distinct (x # xs) == x ~: set xs & distinct xs"
   13.19 +  val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
   13.20 +  val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
   13.21 +  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
   13.22      by (simp add: distinct_def)}
   13.23  
   13.24    fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2