author | haftmann |
Tue, 08 Jan 2008 11:37:32 +0100 | |
changeset 25865 | a141d6bfd398 |
parent 25864 | 11f531354852 |
child 25866 | 263aaf988d44 |
src/Tools/nbe.ML | file | annotate | diff | comparison | revisions |
--- a/src/Tools/nbe.ML Tue Jan 08 11:37:30 2008 +0100 +++ b/src/Tools/nbe.ML Tue Jan 08 11:37:32 2008 +0100 @@ -152,7 +152,7 @@ Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n") (!trace) ("Nbe.univs_ref", univs_ref); -(* code generation with greetings to Tarski *) +(* code generation *) fun assemble_idict (DictConst (inst, dss)) = nbe_apps (nbe_fun inst) ((maps o map) assemble_idict dss)