src/HOL/Hoare_Parallel/Quote_Antiquote.thy
changeset 42284 326f57825e1a
parent 35113 1a0c129bb2e0
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  parse_translation {*
     1.6    let
     1.7 -    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
     1.8 +    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
     1.9        | quote_tr ts = raise TERM ("quote_tr", ts);
    1.10    in [(@{syntax_const "_quote"}, quote_tr)] end
    1.11  *}