diff -r 5ac837d98a85 -r 4988dda71c0b src/FOLP/intprover.ML
--- a/src/FOLP/intprover.ML	Mon Feb 10 12:34:54 1997 +0100
+++ b/src/FOLP/intprover.ML	Mon Feb 10 12:52:11 1997 +0100
@@ -5,12 +5,12 @@
 
 A naive prover for intuitionistic logic
 
-BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
+BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
 
 Completeness (for propositional logic) is proved in 
 
 Roy Dyckhoff.
-Contraction-Free Sequent Calculi for Intuitionistic Logic.
+Contraction-Free Sequent Calculi for IntPruitionistic Logic.
 J. Symbolic Logic (in press)
 *)
 
@@ -27,7 +27,7 @@
   end;
 
 
-structure Int : INT_PROVER   = 
+structure IntPr : INT_PROVER   = 
 struct
 
 (*Negation is treated as a primitive symbol, with rules notI (introduction),