src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50496 8665ec681e47
parent 50495 bd9a0028b063
child 50510 7e4f2f8d9b50
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 15:25:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 15:38:47 2012 +0100
     1.3 @@ -220,8 +220,8 @@
     1.4      fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
     1.5        | is_boring_prop Ts (@{const "==>"} $ t $ u) =
     1.6          is_boring_prop Ts t andalso is_boring_prop Ts u
     1.7 -      | is_boring_prop Ts (Const (@{const_name all}, _) $ (Abs (_, T, t)) $ u) =
     1.8 -        is_boring_prop (T :: Ts) t andalso is_boring_prop (T :: Ts) u
     1.9 +      | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
    1.10 +        is_boring_prop (T :: Ts) t
    1.11        | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
    1.12          is_boring_prop Ts (t $ eta_expand Ts u 1)
    1.13        | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =