diff -r 6f8b1bb4d248 -r 48116a1764c5 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Jul 16 15:28:23 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Jul 16 15:55:32 2010 +0200
@@ -41,11 +41,11 @@
 
   val allow_abort: string -> theory -> theory
   type tyco_syntax = Code_Printer.tyco_syntax
-  type proto_const_syntax = Code_Printer.proto_const_syntax
+  type const_syntax = Code_Printer.const_syntax
   val add_syntax_class: string -> class -> string option -> theory -> theory
   val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
   val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
-  val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
+  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
   val add_include: string -> string * (string * string list) option -> theory -> theory
 end;
@@ -57,7 +57,7 @@
 
 type literals = Code_Printer.literals;
 type tyco_syntax = Code_Printer.tyco_syntax;
-type proto_const_syntax = Code_Printer.proto_const_syntax;
+type const_syntax = Code_Printer.const_syntax;
 
 
 (** basics **)
@@ -83,7 +83,7 @@
   class: string Symtab.table,
   instance: unit Symreltab.table,
   tyco: Code_Printer.tyco_syntax Symtab.table,
-  const: Code_Printer.proto_const_syntax Symtab.table
+  const: Code_Printer.const_syntax Symtab.table
 };
 
 fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -108,7 +108,7 @@
   -> (string -> string option)          (*module aliasses*)
   -> (string -> string option)          (*class syntax*)
   -> (string -> Code_Printer.tyco_syntax option)
-  -> (string -> Code_Printer.const_syntax option)
+  -> (string -> Code_Printer.activated_const_syntax option)
   -> ((Pretty.T -> string) * (Pretty.T -> unit))
   -> Code_Thingol.program
   -> string list                        (*selected statements*)