src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
changeset 42680 b6c27cf04fe9
parent 42671 390de893659a
child 42702 d7c127478ee1
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 04 18:48:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 04 19:35:48 2011 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4       only : bool}
     1.5  
     1.6    val trace : bool Config.T
     1.7 -  val is_global_locality : locality -> bool
     1.8 +  val is_locality_global : locality -> bool
     1.9    val fact_from_ref :
    1.10      Proof.context -> unit Symtab.table -> thm list
    1.11      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    1.12 @@ -70,10 +70,10 @@
    1.13  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
    1.14  
    1.15  (* (quasi-)underapproximation of the truth *)
    1.16 -fun is_global_locality Local = false
    1.17 -  | is_global_locality Assum = false
    1.18 -  | is_global_locality Chained = false
    1.19 -  | is_global_locality _ = true
    1.20 +fun is_locality_global Local = false
    1.21 +  | is_locality_global Assum = false
    1.22 +  | is_locality_global Chained = false
    1.23 +  | is_locality_global _ = true
    1.24  
    1.25  type relevance_fudge =
    1.26    {allow_ext : bool,