src/HOL/Tools/meson.ML
changeset 38786 e46e7a9cb622
parent 38709 04414091f3b5
child 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4      | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
     1.5          if b then prod (signed_nclauses b t) (signed_nclauses b u)
     1.6               else sum (signed_nclauses b t) (signed_nclauses b u)
     1.7 -    | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
     1.8 +    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
     1.9          if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
    1.10               else sum (signed_nclauses (not b) t) (signed_nclauses b u)
    1.11      | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
    1.12 @@ -401,7 +401,7 @@
    1.13    since this code expects to be called on a clause form.*)
    1.14  val is_conn = member (op =)
    1.15      [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
    1.16 -     @{const_name "op -->"}, @{const_name Not},
    1.17 +     @{const_name HOL.implies}, @{const_name Not},
    1.18       @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
    1.19  
    1.20  (*True if the term contains a function--not a logical connective--where the type