src/Tools/Code/code_target.ML
changeset 31957 a9742afd403e
parent 31775 2b04504fcb69
child 32740 9dd0a2f83429
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Jul 07 17:21:26 2009 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Jul 07 17:21:27 2009 +0200
     1.3 @@ -286,7 +286,7 @@
     1.4  fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
     1.5    let
     1.6      val c = prep_const thy raw_c;
     1.7 -    fun check_args (syntax as (n, _)) = if n > Code.no_args thy c
     1.8 +    fun check_args (syntax as (n, _)) = if n > Code.args_number thy c
     1.9        then error ("Too many arguments in syntax for constant " ^ quote c)
    1.10        else syntax;
    1.11    in case raw_syn