reverse order of datatype declarations so that declarations only depend on already declared datatypes
authorboehmes
Thu, 16 Sep 2010 06:49:46 +0200
changeset 39435 5d18f4c00c07
parent 39434 844a9ec44858
child 39436 4a7d09da2b9c
reverse order of datatype declarations so that declarations only depend on already declared datatypes
src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 15 22:24:35 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Sep 16 06:49:46 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)),