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.
merged
authorblanchet
Thu, 16 Sep 2010 14:26:09 +0200
changeset 39458 13c8577e1783
parent 39436 4a7d09da2b9c (diff)
parent 39457 b505208f435d (current diff)
child 39460 6f9765abf984
child 39469 d58b91a9b8b1
child 39491 2416666e6f94
merged
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Sep 16 14:24:48 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Sep 16 14:26:09 2010 +0200
@@ -258,7 +258,7 @@
   header = header,
   sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
   funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [],
-  dtyps = dtyps }
+  dtyps = rev dtyps }
 
 fun make_recon (unfolds, assms) (_, typs, _, _, terms) = {
   typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)),
--- a/src/Tools/nbe.ML	Thu Sep 16 14:24:48 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Sep 16 14:26:09 2010 +0200
@@ -555,6 +555,7 @@
     |> traced (fn _ => "---\n")
   end;
 
+
 (* function store *)
 
 structure Nbe_Functions = Code_Data
isabelle