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