src/HOL/Tools/SMT/smt_normalize.ML
changeset 55414 eab03e9cee8a
parent 54883 dd04a8b654fc
child 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -356,22 +356,22 @@
     1.4  (** rewrite bool case expressions as if expressions **)
     1.5  
     1.6  local
     1.7 -  fun is_bool_case (Const (@{const_name "bool.bool_case"}, _)) = true
     1.8 -    | is_bool_case _ = false
     1.9 +  fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
    1.10 +    | is_case_bool _ = false
    1.11  
    1.12    val thm = mk_meta_eq @{lemma
    1.13 -    "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
    1.14 +    "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
    1.15  
    1.16    fun unfold_conv _ =
    1.17 -    SMT_Utils.if_true_conv (is_bool_case o Term.head_of)
    1.18 +    SMT_Utils.if_true_conv (is_case_bool o Term.head_of)
    1.19        (expand_head_conv (Conv.rewr_conv thm))
    1.20  in
    1.21  
    1.22 -fun rewrite_bool_case_conv ctxt =
    1.23 -  SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
    1.24 +fun rewrite_case_bool_conv ctxt =
    1.25 +  SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
    1.26  
    1.27 -val setup_bool_case =
    1.28 -  SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
    1.29 +val setup_case_bool =
    1.30 +  SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
    1.31  
    1.32  end
    1.33  
    1.34 @@ -558,7 +558,7 @@
    1.35  (** combined unfoldings and rewritings **)
    1.36  
    1.37  fun unfold_conv ctxt =
    1.38 -  rewrite_bool_case_conv ctxt then_conv
    1.39 +  rewrite_case_bool_conv ctxt then_conv
    1.40    unfold_abs_min_max_conv ctxt then_conv
    1.41    nat_as_int_conv ctxt then_conv
    1.42    Thm.beta_conversion true
    1.43 @@ -645,7 +645,7 @@
    1.44    setup_unfolded_quants #>
    1.45    setup_trigger #>
    1.46    setup_weight #>
    1.47 -  setup_bool_case #>
    1.48 +  setup_case_bool #>
    1.49    setup_abs_min_max #>
    1.50    setup_nat_as_int)
    1.51