src/HOL/HOLCF/Tools/fixrec.ML
changeset 47089 29e92b644d6c
parent 46961 5c6955f487e5
child 47432 e1576d13e933
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Mar 22 21:43:26 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Fri Mar 23 20:32:43 2012 +0100
     1.3 @@ -399,7 +399,7 @@
     1.4  
     1.5  val alt_specs' : (bool * (Attrib.binding * string)) list parser =
     1.6    let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
     1.7 -  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
     1.8 +  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"