Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor changes
authornipkow
Fri, 03 Mar 2006 19:43:46 +0100
changeset 19181 5c9f58562602
parent 19180 2b477ae4ece7
child 19182 9b7477a10052
minor changes
src/Pure/Tools/nbe.ML file | annotate | diff | comparison | revisions 
--- 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'')
isabelle