src/HOL/Tools/SMT/smt_normalize.ML
changeset 36936 c52d1c130898
parent 36899 bcd6fce5bf06
child 37153 8feed34275ce
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat May 15 15:31:33 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sat May 15 17:59:06 2010 +0200
     1.3 @@ -47,11 +47,11 @@
     1.4      "distinct [x, y] == (x ~= y)"
     1.5      by simp_all}
     1.6    fun distinct_conv _ =
     1.7 -    if_true_conv is_trivial_distinct (More_Conv.rewrs_conv thms)
     1.8 +    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
     1.9  in
    1.10  fun trivial_distinct ctxt =
    1.11    map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    1.12 -    Conv.fconv_rule (More_Conv.top_conv distinct_conv ctxt))
    1.13 +    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
    1.14  end
    1.15  
    1.16  
    1.17 @@ -67,11 +67,11 @@
    1.18      "(case P of True => x | False => y) == (if P then x else y)"
    1.19      "(case P of False => y | True => x) == (if P then x else y)"
    1.20      by (rule eq_reflection, simp)+}
    1.21 -  val unfold_conv = if_true_conv is_bool_case (More_Conv.rewrs_conv thms)
    1.22 +  val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
    1.23  in
    1.24  fun rewrite_bool_cases ctxt =
    1.25    map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    1.26 -    Conv.fconv_rule (More_Conv.top_conv (K unfold_conv) ctxt))
    1.27 +    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
    1.28  end
    1.29  
    1.30  
    1.31 @@ -107,7 +107,7 @@
    1.32  in
    1.33  fun normalize_numerals ctxt =
    1.34    map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
    1.35 -    Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
    1.36 +    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
    1.37  end
    1.38  
    1.39  
    1.40 @@ -193,7 +193,7 @@
    1.41  local
    1.42    val eta_conv = eta_expand_conv
    1.43  
    1.44 -  fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
    1.45 +  fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt
    1.46    and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt)
    1.47    and keep_let_conv ctxt = Conv.combination_conv
    1.48      (Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt)
    1.49 @@ -267,7 +267,7 @@
    1.50        Conv.binop_conv (atomize_conv ctxt) then_conv
    1.51        Conv.rewr_conv @{thm atomize_eq}
    1.52    | Const (@{const_name all}, _) $ Abs _ =>
    1.53 -      More_Conv.binder_conv atomize_conv ctxt then_conv
    1.54 +      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    1.55        Conv.rewr_conv @{thm atomize_all}
    1.56    | _ => Conv.all_conv) ct
    1.57