src/HOL/HOLCF/Tools/fixrec.ML
changeset 46949 94aa7b81bcf6
parent 46909 3c73a121a387
child 46961 5c6955f487e5
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -391,15 +391,15 @@
     1.4  (*************************************************************************)
     1.5  
     1.6  val opt_thm_name' : (bool * Attrib.binding) parser =
     1.7 -  Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
     1.8 +  @{keyword "("} -- @{keyword "unchecked"} -- @{keyword ")"} >> K (true, Attrib.empty_binding)
     1.9      || Parse_Spec.opt_thm_name ":" >> pair false
    1.10  
    1.11  val spec' : (bool * (Attrib.binding * string)) parser =
    1.12    opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)))
    1.13  
    1.14  val alt_specs' : (bool * (Attrib.binding * string)) list parser =
    1.15 -  let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(")
    1.16 -  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end
    1.17 +  let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
    1.18 +  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
    1.19  
    1.20  val _ =
    1.21    Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl