src/HOL/Hoare_Parallel/Quote_Antiquote.thy
changeset 35113 1a0c129bb2e0
parent 35107 bdca9f765ee4
child 42284 326f57825e1a
     1.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:06:37 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:19:58 2010 +0100
     1.3 @@ -16,9 +16,9 @@
     1.4  
     1.5  parse_translation {*
     1.6    let
     1.7 -    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
     1.8 +    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
     1.9        | quote_tr ts = raise TERM ("quote_tr", ts);
    1.10 -  in [("_quote", quote_tr)] end
    1.11 +  in [(@{syntax_const "_quote"}, quote_tr)] end
    1.12  *}
    1.13  
    1.14  end
    1.15 \ No newline at end of file