diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/Subst.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -26,7 +26,7 @@
 
 defs 
 
-  subst_eq_def  "r =$= s == ALL t.t <| r = t <| s"
+  subst_eq_def  "r =$= s == ALL t. t <| r = t <| s"
 
   comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"