diff -r 56975de9e341 -r 0fd80c27fdf5 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Fri Apr 22 15:25:01 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Fri Apr 22 15:57:43 2011 +0200
@@ -42,12 +42,12 @@
   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
 end;
 
+signature CANCEL_NUMERALS =
+sig
+  val proc: simpset -> term -> thm option
+end;
 
-functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
-  sig
-  val proc: simpset -> term -> thm option
-  end
-=
+functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
 struct
 
 (*For t = #n*u then put u in the table*)