1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -279,7 +279,7 @@
     1.4  val add_partial_function = gen_add_partial_function Specification.check_spec;
     1.5  val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
     1.6  
     1.7 -val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
     1.8 +val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
     1.9  
    1.10  val _ = Outer_Syntax.local_theory
    1.11    "partial_function" "define partial function" Keyword.thy_decl