src/HOL/Tools/SMT/smt_translate.ML
changeset 40579 98ebd2300823
parent 40274 6486c610a549
child 40663 e080c9e68752
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 17 08:14:55 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 17 08:14:56 2010 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4        | (ps, [false]) => cons (SNoPat ps)
     1.5        | _ => raise TERM ("dest_pats", ts))
     1.6  
     1.7 -fun dest_trigger (@{term trigger} $ tl $ t) =
     1.8 +fun dest_trigger (@{const trigger} $ tl $ t) =
     1.9        (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
    1.10    | dest_trigger t = ([], t)
    1.11  
    1.12 @@ -161,8 +161,8 @@
    1.13  
    1.14  val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
    1.15      Const (@{const_name Let}, _) => true
    1.16 -  | @{term "op = :: bool => _"} $ _ $ @{term True} => true
    1.17 -  | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
    1.18 +  | @{const HOL.eq (bool)} $ _ $ @{const True} => true
    1.19 +  | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true
    1.20    | _ => false)
    1.21  
    1.22  val rewrite_rules = [
    1.23 @@ -199,11 +199,11 @@
    1.24      fun conn (n, T) = (n, mapTs as_propT as_propT T)
    1.25      fun pred (n, T) = (n, mapTs I as_propT T)
    1.26  
    1.27 -    val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
    1.28 -    fun as_term t = Const term_eq $ t $ @{term True}
    1.29 +    val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
    1.30 +    fun as_term t = Const term_eq $ t $ @{const True}
    1.31  
    1.32      val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
    1.33 -    fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
    1.34 +    fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
    1.35  
    1.36      fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
    1.37  
    1.38 @@ -225,7 +225,7 @@
    1.39      and in_pats ps =
    1.40        in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
    1.41  
    1.42 -    and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
    1.43 +    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
    1.44        | in_trig t = in_form t
    1.45  
    1.46      and in_form t =