--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Apr 21 21:14:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Apr 21 22:18:28 2011 +0200
@@ -36,6 +36,7 @@
only : bool}
val trace : bool Unsynchronized.ref
+ val is_global_locality : locality -> bool
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
@@ -66,6 +67,12 @@
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
+
type relevance_fudge =
{allow_ext : bool,
local_const_multiplier : real,