1.1 --- a/src/Tools/Code/code_printer.ML	Fri Jul 16 15:28:23 2010 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Fri Jul 16 15:55:32 2010 +0200
     1.3 @@ -67,20 +67,20 @@
     1.4  
     1.5    type tyco_syntax
     1.6    type simple_const_syntax
     1.7 -  type proto_const_syntax
     1.8    type const_syntax
     1.9 +  type activated_const_syntax
    1.10    val parse_infix: ('a -> 'b) -> lrx * int -> string
    1.11      -> int * ((fixity -> 'b -> Pretty.T)
    1.12      -> fixity -> 'a list -> Pretty.T)
    1.13    val parse_syntax: ('a -> 'b) -> Token.T list
    1.14      -> (int * ((fixity -> 'b -> Pretty.T)
    1.15      -> fixity -> 'a list -> Pretty.T)) option * Token.T list
    1.16 -  val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    1.17 +  val simple_const_syntax: simple_const_syntax -> const_syntax
    1.18    val activate_const_syntax: theory -> literals
    1.19 -    -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    1.20 +    -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
    1.21    val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    1.22      -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.23 -    -> (string -> const_syntax option)
    1.24 +    -> (string -> activated_const_syntax option)
    1.25      -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    1.26    val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.27      -> thm option -> fixity
    1.28 @@ -243,10 +243,10 @@
    1.29  
    1.30  type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
    1.31    -> fixity -> (iterm * itype) list -> Pretty.T);
    1.32 -type proto_const_syntax = int * (string list * (literals -> string list
    1.33 +type const_syntax = int * (string list * (literals -> string list
    1.34    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    1.35      -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    1.36 -type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.37 +type activated_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.38    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.39  
    1.40  fun simple_const_syntax syn =