tuning
authorblanchet
Wed Sep 07 13:50:17 2011 +0200 (2011-09-07)
changeset 447833634c6dba23f
parent 44782 ba4c0205267f
child 44784 c9a081ef441d
tuning
src/HOL/Tools/ATP/atp_reconstruct.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Sep 07 13:50:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4      union (op =) (resolve_fact facts_offset fact_names name)
     1.5    | add_fact ctxt _ _ (Inference (_, _, deps)) =
     1.6      if AList.defined (op =) deps leo2_ext then
     1.7 -      insert (op =) (ext_name ctxt, Extensionality)
     1.8 +      insert (op =) (ext_name ctxt, General)
     1.9      else
    1.10        I
    1.11    | add_fact _ _ _ _ = I
     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:16 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     2.3 @@ -16,8 +16,7 @@
     2.4    type 'a problem = 'a ATP_Problem.problem
     2.5  
     2.6    datatype locality =
     2.7 -    General | Helper | Induction | Extensionality | Intro | Elim | Simp |
     2.8 -    Local | Assum | Chained
     2.9 +    General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
    2.10  
    2.11    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    2.12    datatype soundness = Sound_Modulo_Infiniteness | Sound
    2.13 @@ -526,8 +525,7 @@
    2.14      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
    2.15  
    2.16  datatype locality =
    2.17 -  General | Helper | Induction | Extensionality | Intro | Elim | Simp |
    2.18 -  Local | Assum | Chained
    2.19 +  General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
    2.20  
    2.21  datatype order = First_Order | Higher_Order
    2.22  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:16 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 07 13:50:17 2011 +0200
     3.3 @@ -144,7 +144,6 @@
     3.4                   (j + 1,
     3.5                    ((nth_name j,
     3.6                      if member Thm.eq_thm_prop chained_ths th then Chained
     3.7 -                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
     3.8                      else General), th) :: rest))
     3.9      |> snd
    3.10    end
    3.11 @@ -845,8 +844,7 @@
    3.12        else if global then
    3.13          case Termtab.lookup clasimpset_table (prop_of th) of
    3.14            SOME loc => loc
    3.15 -        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
    3.16 -                  else General
    3.17 +        | NONE => General
    3.18        else if is_assum th then Assum else Local
    3.19      fun is_good_unnamed_local th =
    3.20        not (Thm.has_name_hint th) andalso