diff -r 2054fa3c8d76 -r 45a789407806 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Nov 25 00:01:04 1994 +0100
+++ b/src/FOL/simpdata.ML	Fri Nov 25 00:02:37 1994 +0100
@@ -114,6 +114,7 @@
   prove_goal FOL.thy s
    (fn prems => [ (cut_facts_tac prems 1), 
 		  (Cla.fast_tac FOL_cs 1) ]));
+
 val cla_rews = map prove_fun
  ["~(P&Q)  <-> ~P | ~Q",
   "P | ~P", 		"~P | P",