# HG changeset patch
# User nipkow
# Date 1141411426 -3600
# Node ID 5c9f58562602494c6b1990159ea72fc1dfb1ec72
# Parent  2b477ae4ece7437be4f577ce7df6d479319d1360
minor changes

diff -r 2b477ae4ece7 -r 5c9f58562602 src/Pure/Tools/nbe.ML
--- a/src/Pure/Tools/nbe.ML	Fri Mar 03 19:30:30 2006 +0100
+++ b/src/Pure/Tools/nbe.ML	Fri Mar 03 19:43:46 2006 +0100
@@ -51,8 +51,14 @@
              Library.seq (use_show o NBE_Codegen.generate defined) diff);
     val thy'' = NBE_Data.put (!tab) thy';
     val nt' = NBE_Eval.nbe (!tab) t';
+    val _ = print nt';
     val t' = NBE_Codegen.nterm_to_term thy'' nt';
-    val _ = print nt';
+(*
+    val _ = print t';
+    val (t'', _) =
+      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) (K NONE) (K NONE)
+        [] true ([t'], type_of t);
+*)
     val _ = (Pretty.writeln o Sign.pretty_term thy'') t';
   in
     (t', thy'')