consolidate const_syntax naming

--- a/src/Tools/Code/code_printer.ML	Fri Jul 16 15:28:23 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Fri Jul 16 15:55:32 2010 +0200
@@ -67,20 +67,20 @@
 
   type tyco_syntax
   type simple_const_syntax
-  type proto_const_syntax
   type const_syntax
+  type activated_const_syntax
   val parse_infix: ('a -> 'b) -> lrx * int -> string
     -> int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)
   val parse_syntax: ('a -> 'b) -> Token.T list
     -> (int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)) option * Token.T list
-  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
+  val simple_const_syntax: simple_const_syntax -> const_syntax
   val activate_const_syntax: theory -> literals
-    -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
+    -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
   val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-    -> (string -> const_syntax option)
+    -> (string -> activated_const_syntax option)
     -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> fixity
@@ -243,10 +243,10 @@
 
 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   -> fixity -> (iterm * itype) list -> Pretty.T);
-type proto_const_syntax = int * (string list * (literals -> string list
+type const_syntax = int * (string list * (literals -> string list
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
-type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+type activated_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
   -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
 fun simple_const_syntax syn =

--- 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*)