src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
changeset 44783 3634c6dba23f
parent 44625 4a1132815a70
child 44785 f4975fa4a2f8
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -144,7 +144,6 @@
     1.4                   (j + 1,
     1.5                    ((nth_name j,
     1.6                      if member Thm.eq_thm_prop chained_ths th then Chained
     1.7 -                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
     1.8                      else General), th) :: rest))
     1.9      |> snd
    1.10    end
    1.11 @@ -845,8 +844,7 @@
    1.12        else if global then
    1.13          case Termtab.lookup clasimpset_table (prop_of th) of
    1.14            SOME loc => loc
    1.15 -        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
    1.16 -                  else General
    1.17 +        | NONE => General
    1.18        else if is_assum th then Assum else Local
    1.19      fun is_good_unnamed_local th =
    1.20        not (Thm.has_name_hint th) andalso