--- a/src/HOL/ex/Multiquote.thy Thu Mar 30 20:06:27 2000 +0200
+++ b/src/HOL/ex/Multiquote.thy Thu Mar 30 21:26:10 2000 +0200
@@ -40,6 +40,6 @@
term ".(.(` `x + `y).).";
term ".(.(` `x + `y). o `f).";
term ".(`(f o `g)).";
-term ".(.(`(`(f o `g))).).";
+term ".(.( ` `(f o `g) ).).";
end;