1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 18:46:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 18:46:38 2014 +0200
     1.3 @@ -68,13 +68,11 @@
     1.4  fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
     1.5    | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
     1.6  
     1.7 -fun is_True_prop t = t aconv @{prop True}
     1.8 -
     1.9  fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
    1.10      (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
    1.11         definitions. *)
    1.12      if role = Conjecture orelse role = Negated_Conjecture then line :: lines
    1.13 -    else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines
    1.14 +    else if t aconv @{prop True} then map (replace_dependencies_in_line (name, [])) lines
    1.15      else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
    1.16      else if role = Axiom then lines (* axioms (facts) need no proof lines *)
    1.17      else map (replace_dependencies_in_line (name, [])) lines
    1.18 @@ -83,18 +81,16 @@
    1.19  fun add_lines_pass2 res _ [] = rev res
    1.20    | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) =
    1.21      let
    1.22 -      val is_last_line = null lines
    1.23 -
    1.24 -      fun looks_interesting () =
    1.25 -        not (is_True_prop t) andalso not (t aconv prev_t) andalso null (Term.add_tvars t []) andalso
    1.26 -        length deps >= 2 andalso not (can the_single lines)
    1.27 +      fun looks_boring () =
    1.28 +        t aconv @{prop True} orelse t aconv @{prop False} orelse t aconv prev_t orelse
    1.29 +        length deps < 2
    1.30  
    1.31        fun is_skolemizing_line (_, _, _, rule', deps') =
    1.32          is_skolemize_rule rule' andalso member (op =) deps' name
    1.33        fun is_before_skolemize_rule () = exists is_skolemizing_line lines
    1.34      in
    1.35        if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
    1.36 -         is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
    1.37 +         is_datatype_rule rule orelse null lines orelse not (looks_boring ()) orelse
    1.38           is_before_skolemize_rule () then
    1.39          add_lines_pass2 (line :: res) t lines
    1.40        else