diff -r f4cecad9b6a0 -r 3751567696bf src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Apr 04 17:20:15 1994 +0200
+++ b/src/Pure/thm.ML	Wed Apr 06 16:36:34 1994 +0200
@@ -5,7 +5,6 @@
 
 The abstract types "theory" and "thm".
 Also "cterm" / "ctyp" (certified terms / typs under a signature).
-
 *)
 
 signature THM =
@@ -103,7 +102,7 @@
 end;
 
 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN
-  and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)(*: THM *) (* FIXME debug *) =
+  and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) : THM =
 struct
 
 structure Sequence = Unify.Sequence;
@@ -599,7 +598,7 @@
   end
   handle TERM _ => raise THM("dest_state", i, [state]);
 
-(*Increment variables and parameters of rule as required for
+(*Increment variables and parameters of orule as required for
   resolution with goal i of state. *)
 fun lift_rule (state, i) orule =
   let val Thm{prop=sprop,maxidx=smax,...} = state;