src/Tools/Code/code_target.ML
changeset 39291 c6d146ed07ae
parent 39290 fa197571676b
child 39292 551fe1af03b0
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 13:58:16 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 14:36:49 2010 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    val cert_tyco: theory -> string -> string
     1.6    val read_tyco: theory -> string -> string
     1.7 +  val read_const_exprs: theory -> string list -> string list
     1.8  
     1.9    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    1.10      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    1.11 @@ -77,7 +78,7 @@
    1.12  
    1.13  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    1.14    | serialization _ string content width Produce = SOME (string [] width content)
    1.15 -  | serialization _ string content width (Present _) = SOME (string [] width content);
    1.16 +  | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
    1.17  
    1.18  fun export some_path f = (f (Export some_path); ());
    1.19  fun produce f = the (f Produce);