src/Tools/Code/code_namespace.ML
changeset 59103 788db6d6b8a5
parent 59058 a78612c67ec0
child 67521 6a27e86cc2e7
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    type flat_program
     1.5    val flat_program: Proof.context
     1.6      -> { module_prefix: string, module_name: string,
     1.7 -    reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
     1.8 +    reserved: Name.context, identifiers: Code_Printer.identifiers, empty_nsp: 'a,
     1.9      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
    1.10      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
    1.11        -> Code_Symbol.T list -> Code_Thingol.program
    1.12 @@ -30,7 +30,7 @@
    1.13    type ('a, 'b) hierarchical_program
    1.14    val hierarchical_program: Proof.context
    1.15      -> { module_name: string,
    1.16 -    reserved: Name.context, identifiers: Code_Target.identifier_data,
    1.17 +    reserved: Name.context, identifiers: Code_Printer.identifiers,
    1.18      empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    1.19      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    1.20      cyclic_modules: bool,