# HG changeset patch
# User boehmes
# Date 1284612586 -7200
# Node ID 5d18f4c00c07af421bce618547fdaea1b78fa5e4
# Parent  844a9ec448584fffaa684e4ad39c1e7f68d75289
reverse order of datatype declarations so that declarations only depend on already declared datatypes

diff -r 844a9ec44858 -r 5d18f4c00c07 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)),