src/FOLP/ROOT.ML
changeset 3836 f1a1817659e6
parent 3511 da4dd8b7ced4
child 3942 1f1c1f524d19
--- a/src/FOLP/ROOT.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ROOT.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -33,7 +33,7 @@
 
   (*etac rev_cut_eq moves an equality to be the last premise. *)
   val rev_cut_eq = prove_goal IFOLP.thy 
-                "[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
+                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
 
   val rev_mp = rev_mp