# HG changeset patch
# User wenzelm
# Date 954003687 -3600
# Node ID 3b9e3c782eb2e8a1838b2214cc54eb781aed0d53
# Parent  4a3cdf01531bbcd230d115ba29e223225259a5d1
tuned;

diff -r 4a3cdf01531b -r 3b9e3c782eb2 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Sat Mar 25 17:59:52 2000 +0100
+++ b/src/HOL/ex/Multiquote.thy	Sat Mar 25 18:01:27 2000 +0100
@@ -9,8 +9,8 @@
 theory Multiquote = Main:;
 
 syntax
-  "_quote" :: "'b => ('a => 'b)"	     ("{._.}" [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 999);
+  "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
+  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 1000);
 
 parse_translation {*
   let
@@ -25,21 +25,21 @@
           c $ skip_antiquote_tr i t
       | skip_antiquote_tr i t = antiquote_tr i t;
 
-    fun quote_tr [t] = Abs ("state", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
+    fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [("_quote", quote_tr)] end
 *};
 
 text {* basic examples *};
-term "{. a + b + c .}";
-term "{. a + b + c + `x + `y + 1 .}";
-term "{. `(f w) + `x .}";
-term "{. f (`x) (`y) z .}";
+term ".(a + b + c).";
+term ".(a + b + c + `x + `y + 1).";
+term ".(`(f w) + `x).";
+term ".(f `x `y z).";
 
 text {* advanced examples *};
-term "{. {. `(`x) + `y .} .}";
-term "{. {. `(`x) + `y .} o `f .}";
-term "{. `(f o `g) .}";
-term "{. {. `(`(f o `g)) .} .}";
+term ".(.(` `x + `y).).";
+term ".(.(` `x + `y). o `f).";
+term ".(`(f o `g)).";
+term ".(.(`(`(f o `g))).).";
 
 end;