diff -r 75b01355e5d4 -r b350516cb1f9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -53,10 +53,9 @@
   };
   val pred_compfuns : compilation_funs
   val randompred_compfuns : compilation_funs
-    (*  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
-  *)
 end;
 
 structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =