# HG changeset patch
# User wenzelm
# Date 954444370 -7200
# Node ID 44ec33bb5c5b899815e9f8396af460f543bc3810
# Parent  76e3913ff421cc493a061043d1c180fb2d4f2871
tuned;

diff -r 76e3913ff421 -r 44ec33bb5c5b src/HOL/ex/Multiquote.thy
--- 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;