1.1 --- a/src/HOL/ex/Multiquote.thy	Fri Mar 24 20:59:15 2000 +0100
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Fri Mar 24 21:09:34 2000 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  theory Multiquote = Main:;
     1.5  
     1.6  syntax
     1.7 -  "_quote" :: "'b \\<Rightarrow> ('a \\<Rightarrow> 'b)"	     ("{._.}" [0] 1000)
     1.8 -  "_antiquote" :: "('a \\<Rightarrow> 'b) \\<Rightarrow> 'b"        ("`_" [1000] 999);
     1.9 +  "_quote" :: "'b => ('a => 'b)"	     ("{._.}" [0] 1000)
    1.10 +  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 999);
    1.11  
    1.12  parse_translation {*
    1.13    let