# HG changeset patch
# User wenzelm
# Date 953928574 -3600
# Node ID 794843a9d8b1df0f75c225198520beacddb39fe7
# Parent  c323613e4a47c420803e0feaea4981623cdf0ea1
plain ASCII;

diff -r c323613e4a47 -r 794843a9d8b1 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Fri Mar 24 20:59:15 2000 +0100
+++ b/src/HOL/ex/Multiquote.thy	Fri Mar 24 21:09:34 2000 +0100
@@ -9,8 +9,8 @@
 theory Multiquote = Main:;
 
 syntax
-  "_quote" :: "'b \\<Rightarrow> ('a \\<Rightarrow> 'b)"	     ("{._.}" [0] 1000)
-  "_antiquote" :: "('a \\<Rightarrow> 'b) \\<Rightarrow> 'b"        ("`_" [1000] 999);
+  "_quote" :: "'b => ('a => 'b)"	     ("{._.}" [0] 1000)
+  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 999);
 
 parse_translation {*
   let