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.
Fixed bug in code generator for primitive definitions that
authorberghofe
Thu, 26 Jan 2006 17:58:01 +0100
changeset 18788 4f4ed2a01152
parent 18787 5784fe1b5657
child 18789 8a5c6fc3ad27
Fixed bug in code generator for primitive definitions that caused dependencies to get mixed up.
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/codegen.ML	Thu Jan 26 15:37:14 2006 +0100
+++ b/src/Pure/codegen.ML	Thu Jan 26 17:58:01 2006 +0100
@@ -763,7 +763,7 @@
                  NONE =>
                    let
                      val _ = message ("expanding definition of " ^ s);
-                     val (Ts, _) = strip_type T;
+                     val (Ts, _) = strip_type U;
                      val (args', rhs') =
                        if not (null args) orelse null Ts then (args, rhs) else
                          let val v = Free (new_name rhs "x", hd Ts)
isabelle