src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
changeset 51877 71052c42edf2
parent 51179 0d5f8812856f
child 52110 411db77f96f2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon May 06 11:03:08 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon May 06 11:03:08 2013 +0200
     1.3 @@ -134,8 +134,8 @@
     1.4          if p <> cp then
     1.5            (env, cp + 1, ps, annots)
     1.6          else
     1.7 -          let val (_, (env', T')) = get_annot env T in
     1.8 -            (env', cp + 1, ps', (p, T') :: annots)
     1.9 +          let val (annot_necessary, (env', T')) = get_annot env T in
    1.10 +            (env', cp + 1, ps', annots |> annot_necessary ? cons (p, T'))
    1.11            end
    1.12        | post1 _ _ accum = accum
    1.13      val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'