src/HOL/Tools/SMT/smt_normalize.ML
changeset 47155 ade3fc826af3
parent 47108 2a1953f0d20d
child 47207 9368aa814518
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Mar 27 17:11:02 2012 +0200
     1.3 @@ -346,32 +346,6 @@
     1.4  
     1.5  (* unfolding of definitions and theory-specific rewritings *)
     1.6  
     1.7 -(** unfold trivial distincts **)
     1.8 -
     1.9 -local
    1.10 -  fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
    1.11 -        (case try HOLogic.dest_list t of
    1.12 -          SOME [] => true
    1.13 -        | SOME [_] => true
    1.14 -        | _ => false)
    1.15 -    | is_trivial_distinct _ = false
    1.16 -
    1.17 -  val thms = map mk_meta_eq @{lemma
    1.18 -    "distinct [] = True"
    1.19 -    "distinct [x] = True"
    1.20 -    "distinct [x, y] = (x ~= y)"
    1.21 -    by simp_all}
    1.22 -  fun distinct_conv _ =
    1.23 -    SMT_Utils.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.24 -in
    1.25 -
    1.26 -fun trivial_distinct_conv ctxt =
    1.27 -  SMT_Utils.if_exists_conv is_trivial_distinct
    1.28 -    (Conv.top_conv distinct_conv ctxt)
    1.29 -
    1.30 -end
    1.31 -
    1.32 -
    1.33  (** rewrite bool case expressions as if expressions **)
    1.34  
    1.35  local
    1.36 @@ -573,7 +547,6 @@
    1.37  (** combined unfoldings and rewritings **)
    1.38  
    1.39  fun unfold_conv ctxt =
    1.40 -  trivial_distinct_conv ctxt then_conv
    1.41    rewrite_bool_case_conv ctxt then_conv
    1.42    unfold_abs_min_max_conv ctxt then_conv
    1.43    nat_as_int_conv ctxt then_conv