src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 56100 0dc5f68a7802
parent 56090 34bd10a9a2ad
child 56103 6689512f3710
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:14 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -49,8 +49,7 @@
     1.4    (case Thm.prop_of thm of
     1.5      @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
     1.6        norm_def (thm RS @{thm fun_cong})
     1.7 -  | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
     1.8 -      norm_def (thm RS @{thm meta_eq_to_obj_eq})
     1.9 +  | Const (@{const_name "=="}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    1.10    | _ => thm)
    1.11  
    1.12  
    1.13 @@ -368,8 +367,7 @@
    1.14  (** unfold abs, min and max **)
    1.15  
    1.16  local
    1.17 -  val abs_def = mk_meta_eq @{lemma
    1.18 -    "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
    1.19 +  val abs_def = mk_meta_eq @{lemma "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
    1.20      by (rule ext) (rule abs_if)}
    1.21  
    1.22    val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
    1.23 @@ -381,13 +379,10 @@
    1.24    val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
    1.25      (@{const_name abs}, abs_def)]
    1.26  
    1.27 -  fun is_builtinT ctxt T =
    1.28 -    SMT2_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
    1.29 -
    1.30 -  fun abs_min_max ctxt (Const (n, T)) =
    1.31 +  fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
    1.32          (case AList.lookup (op =) defs n of
    1.33            NONE => NONE
    1.34 -        | SOME thm => if is_builtinT ctxt T then SOME thm else NONE)
    1.35 +        | SOME thm => if SMT2_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE)
    1.36      | abs_min_max _ _ = NONE
    1.37  
    1.38    fun unfold_amm_conv ctxt ct =
    1.39 @@ -498,8 +493,7 @@
    1.40  val nat_as_int_conv = nat_conv
    1.41  
    1.42  fun add_nat_embedding thms =
    1.43 -  if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding)
    1.44 -  else (thms, [])
    1.45 +  if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, [])
    1.46  
    1.47  val setup_nat_as_int =
    1.48    SMT2_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>