src/HOL/Tools/SMT/smt_translate.ML
changeset 39435 5d18f4c00c07
parent 39298 5aefb5bc8a93
child 39483 9f0e5684f04b
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 15 22:24:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Sep 16 06:49:46 2010 +0200
     1.3 @@ -258,7 +258,7 @@
     1.4    header = header,
     1.5    sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
     1.6    funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [],
     1.7 -  dtyps = dtyps }
     1.8 +  dtyps = rev dtyps }
     1.9  
    1.10  fun make_recon (unfolds, assms) (_, typs, _, _, terms) = {
    1.11    typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)),