src/HOL/Tools/SMT/smt_normalize.ML
changeset 40681 872b08416fb4
parent 40663 e080c9e68752
child 40685 dcb27631cb45
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 08:51:48 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 10:39:58 2010 +0100
     1.3 @@ -39,18 +39,18 @@
     1.4     three elements in the argument list) *)
     1.5  
     1.6  local
     1.7 -  fun is_trivial_distinct (Const (@{const_name SMT.distinct}, _) $ t) =
     1.8 -       (length (HOLogic.dest_list t) <= 2
     1.9 -        handle TERM _ => error ("SMT: constant " ^
    1.10 -          quote @{const_name SMT.distinct} ^ " must be applied to " ^
    1.11 -          "an explicit list."))
    1.12 +  fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
    1.13 +        (case try HOLogic.dest_list t of
    1.14 +          SOME [] => true
    1.15 +        | SOME [_] => true
    1.16 +        | _ => false)
    1.17      | is_trivial_distinct _ = false
    1.18  
    1.19    val thms = map mk_meta_eq @{lemma
    1.20 -    "SMT.distinct [] = True"
    1.21 -    "SMT.distinct [x] = True"
    1.22 -    "SMT.distinct [x, y] = (x ~= y)"
    1.23 -    by (simp_all add: distinct_def)}
    1.24 +    "distinct [] = True"
    1.25 +    "distinct [x] = True"
    1.26 +    "distinct [x, y] = (x ~= y)"
    1.27 +    by simp_all}
    1.28    fun distinct_conv _ =
    1.29      U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.30  in