src/HOL/BNF/Tools/bnf_def.ML
changeset 51787 1267c28c7bdd
parent 51767 bbcdd8519253
child 51790 22517d04d20b
     1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Apr 26 09:53:11 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Apr 26 11:04:45 2013 +0200
     1.3 @@ -1320,7 +1320,7 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
     1.7 -    ((parse_opt_binding_colon -- Parse.term --
     1.8 +    ((parse_opt_binding_colon Binding.empty -- Parse.term --
     1.9         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
    1.10         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
    1.11         >> bnf_def_cmd);