1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4          do_quantifier (pos = SOME true) body_t
     1.5        | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
     1.6        | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
     1.7 -      | @{const "op -->"} $ t1 $ t2 =>
     1.8 +      | @{const HOL.implies} $ t1 $ t2 =>
     1.9          do_formula (flip pos) t1 #> do_formula pos t2
    1.10        | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
    1.11          fold (do_term_or_formula T) [t1, t2]
    1.12 @@ -541,7 +541,7 @@
    1.13        | (_, @{const "==>"} $ t1 $ t2) =>
    1.14          do_formula (not pos) t1 andalso
    1.15          (t2 = @{prop False} orelse do_formula pos t2)
    1.16 -      | (_, @{const "op -->"} $ t1 $ t2) =>
    1.17 +      | (_, @{const HOL.implies} $ t1 $ t2) =>
    1.18          do_formula (not pos) t1 andalso
    1.19          (t2 = @{const False} orelse do_formula pos t2)
    1.20        | (_, @{const Not} $ t1) => do_formula (not pos) t1