--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Oct 29 18:17:04 2010 +0200
@@ -40,15 +40,18 @@
three elements in the argument list) *)
local
- fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
- length (HOLogic.dest_list t) <= 2
+ fun is_trivial_distinct (Const (@{const_name SMT.distinct}, _) $ t) =
+ (length (HOLogic.dest_list t) <= 2
+ handle TERM _ => error ("SMT: constant " ^
+ quote @{const_name SMT.distinct} ^ " must be applied to " ^
+ "an explicit list."))
| is_trivial_distinct _ = false
val thms = map mk_meta_eq @{lemma
- "distinct [] = True"
- "distinct [x] = True"
- "distinct [x, y] = (x ~= y)"
- by simp_all}
+ "SMT.distinct [] = True"
+ "SMT.distinct [x] = True"
+ "SMT.distinct [x, y] = (x ~= y)"
+ by (simp_all add: distinct_def)}
fun distinct_conv _ =
if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
in