--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed May 04 18:48:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed May 04 19:35:48 2011 +0200
@@ -36,7 +36,7 @@
only : bool}
val trace : bool Config.T
- val is_global_locality : locality -> bool
+ val is_locality_global : locality -> bool
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
@@ -70,10 +70,10 @@
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
(* (quasi-)underapproximation of the truth *)
-fun is_global_locality Local = false
- | is_global_locality Assum = false
- | is_global_locality Chained = false
- | is_global_locality _ = true
+fun is_locality_global Local = false
+ | is_locality_global Assum = false
+ | is_locality_global Chained = false
+ | is_locality_global _ = true
type relevance_fudge =
{allow_ext : bool,