# HG changeset patch
# User boehmes
# Date 1269644255 -3600
# Node ID 344afccb09d114079df974bc074773013a4c42eb
# Parent  b88e061754a1c65b7858c678b7a2614adaac5ee6
made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)

diff -r b88e061754a1 -r 344afccb09d1 src/HOL/SMT/Tools/smt_translate.ML
--- a/src/HOL/SMT/Tools/smt_translate.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Fri Mar 26 23:57:35 2010 +0100
@@ -433,21 +433,26 @@
     in fresh_name (p, i) ||> (fn (_, i') => (nT, ((pf, pp), i'))) end
 
   val empty_sign = (Typtab.empty, Termtab.empty, Termtab.empty)
-  fun lookup_typ (typs, _, _) = Typtab.lookup typs
-  fun lookup_fun true (_, funs, _) = Termtab.lookup funs
-    | lookup_fun false (_, _, preds) = Termtab.lookup preds
-  fun add_typ x (typs, funs, preds) = (Typtab.update x typs, funs, preds)
-  fun add_fun true x (typs, funs, preds) = (typs, Termtab.update x funs, preds)
-    | add_fun false x (typs, funs, preds) = (typs, funs, Termtab.update x preds)
+  fun lookup_typ (typs, _, _) = Option.map snd o Typtab.lookup typs
+  fun lookup_fun true (_, funs, _) = Option.map snd o Termtab.lookup funs
+    | lookup_fun false (_, _, preds) = Option.map snd o Termtab.lookup preds
+  fun ext (k, v) = (k, (serial (), v))
+  fun p_ord p = prod_ord int_ord (K EQUAL) p
+  fun add_typ x (typs, funs, preds) =
+    (Typtab.update (ext x) typs, funs, preds)
+  fun add_fun true x (typs, funs, preds) =
+        (typs, Termtab.update (ext x) funs, preds)
+    | add_fun false x (typs, funs, preds) =
+        (typs, funs, Termtab.update (ext x) preds)
   fun make_sign (typs, funs, preds) = {
-    typs = map snd (Typtab.dest typs),
-    funs = map snd (Termtab.dest funs),
-    preds = map (apsnd fst o snd) (Termtab.dest preds) }
+    typs = map snd (sort p_ord (map snd (Typtab.dest typs))),
+    funs = map snd (sort p_ord (map snd (Termtab.dest funs))),
+    preds = map (apsnd fst o snd) (sort p_ord (map snd (Termtab.dest preds))) }
   fun make_rtab (typs, funs, preds) =
     let
-      val rTs = Typtab.dest typs |> map swap |> Symtab.make
+      val rTs = Typtab.dest typs |> map (swap o apsnd snd) |> Symtab.make
       val rts = Termtab.dest funs @ Termtab.dest preds
-        |> map (apfst fst o swap) |> Symtab.make
+        |> map (apfst fst o swap o apsnd snd) |> Symtab.make
     in {typs=rTs, terms=rts} end
 
   fun either f g x = (case f x of NONE => g x | y => y)