diff -r 41ce0b56d858 -r 7f11d833d65b src/Tools/Metis/src/Thm.sig
--- a/src/Tools/Metis/src/Thm.sig	Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sig	Mon Sep 13 21:24:10 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
-(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSES                                  *)
-(* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *)
+(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS                         *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
 (* ========================================================================= *)
 
 signature Thm =
@@ -10,6 +10,12 @@
 (* An abstract type of first order logic theorems.                           *)
 (* ------------------------------------------------------------------------- *)
 
+type thm
+
+(* ------------------------------------------------------------------------- *)
+(* Theorem destructors.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
 type clause = LiteralSet.set
 
 datatype inferenceType =
@@ -21,14 +27,8 @@
   | Refl
   | Equality
 
-type thm
-
 type inference = inferenceType * thm list
 
-(* ------------------------------------------------------------------------- *)
-(* Theorem destructors.                                                      *)
-(* ------------------------------------------------------------------------- *)
-
 val clause : thm -> clause
 
 val inference : thm -> inference
@@ -79,11 +79,11 @@
 (* Pretty-printing.                                                          *)
 (* ------------------------------------------------------------------------- *)
 
-val ppInferenceType : inferenceType Parser.pp
+val ppInferenceType : inferenceType Print.pp
 
 val inferenceTypeToString : inferenceType -> string
 
-val pp : thm Parser.pp
+val pp : thm Print.pp
 
 val toString : thm -> string