--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Mar 31 16:44:41 2010 +0200
@@ -7,12 +7,12 @@
signature PREDICATE_COMPILE =
sig
val setup : theory -> theory
- val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
+ val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory
val present_graph : bool Unsynchronized.ref
val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
end;
-structure Predicate_Compile (*: PREDICATE_COMPILE*) =
+structure Predicate_Compile : PREDICATE_COMPILE =
struct
val present_graph = Unsynchronized.ref false