--- a/src/Pure/Tools/nbe.ML Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe.ML Wed Mar 01 13:47:42 2006 +0100
@@ -44,8 +44,9 @@
val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
(CodegenPackage.get_root_module thy);
val (t', thy') = CodegenPackage.codegen_term t thy
- val modl_new = CodegenPackage.get_root_module thy;
- val diff = CodegenThingol.diff_module (modl_old, modl_new);
+ val modl_new = CodegenPackage.get_root_module thy';
+ val diff = CodegenThingol.diff_module (modl_new, modl_old);
+ val _ = writeln ("new definitions: " ^ (commas o map fst) diff);
val _ = (tab := nbe_tab;
Library.seq (use_show o NBE_Codegen.generate defined) diff)
val thy'' = NBE_Data.put (!tab) thy'