src/Tools/Code/code_target.ML
changeset 34081 bb01fd325c6b
parent 34071 93bfbb557e2e
child 34152 8e5b596d8c73
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Dec 14 09:53:34 2009 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Dec 14 10:13:06 2009 +0100
     1.3 @@ -405,23 +405,23 @@
     1.4      | NONE => (map_name_syntax target o mapp) (del x) thy
     1.5    end;
     1.6  
     1.7 -val gen_add_syntax_class =
     1.8 -  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) I;
     1.9 +fun gen_add_syntax_class prep =
    1.10 +  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) I prep;
    1.11  
    1.12 -val gen_add_syntax_inst =
    1.13 -  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) I;
    1.14 +fun gen_add_syntax_inst prep =
    1.15 +  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) I prep;
    1.16  
    1.17 -val gen_add_syntax_tyco =
    1.18 +fun gen_add_syntax_tyco prep =
    1.19    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
    1.20      (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
    1.21        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
    1.22 -      else ()) I;
    1.23 +      else ()) I prep;
    1.24  
    1.25 -val gen_add_syntax_const =
    1.26 +fun gen_add_syntax_const prep =
    1.27    gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
    1.28      (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
    1.29        then error ("Too many arguments in syntax for constant " ^ quote c)
    1.30 -      else ()) I;
    1.31 +      else ()) I prep;
    1.32  
    1.33  fun add_reserved target =
    1.34    let