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