--- a/src/HOL/ex/Multiquote.thy Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/ex/Multiquote.thy Thu Feb 11 22:19:58 2010 +0100
@@ -1,11 +1,12 @@
(* Title: HOL/ex/Multiquote.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
header {* Multiple nested quotations and anti-quotations *}
-theory Multiquote imports Main begin
+theory Multiquote
+imports Main
+begin
text {*
Multiple nested quotations and anti-quotations -- basically a
@@ -13,25 +14,25 @@
*}
syntax
- "_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
+ "_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
+ "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
parse_translation {*
let
- fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
- skip_antiquote_tr i t
- | antiquote_tr i (Const ("_antiquote", _) $ t) =
+ fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
+ (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
+ | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) =
antiquote_tr i t $ Bound i
| antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
| antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
| antiquote_tr _ a = a
- and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
+ and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) =
c $ skip_antiquote_tr i t
| skip_antiquote_tr i t = antiquote_tr i 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
+ in [(@{syntax_const "_quote"}, quote_tr)] end
*}
text {* basic examples *}