reverse order of datatype declarations so that declarations only depend on already declared datatypes
--- 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)),