--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri May 28 13:49:21 2010 +0200
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_FACT_PREPROCESSOR =
sig
+ val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
val skolem_prefix: string
@@ -31,6 +32,9 @@
open Sledgehammer_FOL_Clause
+(* Used to label theorems chained into the goal. *)
+val chained_prefix = "Sledgehammer.chained_"
+
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();