# HG changeset patch
# User bulwahn
# Date 1270046681 -7200
# Node ID 88203782cf12a40536aa4cb0090c732af9316efd
# Parent  0ce5b7a5c2fdfece80bfa5d4ff536376896b923f
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes

diff -r 0ce5b7a5c2fd -r 88203782cf12 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- 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