# HG changeset patch
# User blanchet
# Date 1288349345 -7200
# Node ID b91e2e16d994351fd2334cd079ea4e7dc9fb5764
# Parent  51ed7a5ad4c5b5ddab9549c8039abdde6ac7cc6c
fixed order of quantifier instantiation in new Skolemizer

diff -r 51ed7a5ad4c5 -r b91e2e16d994 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
@@ -682,8 +682,11 @@
       THEN' release_clusters_tac thy ax_counts substs clusters
     end
 
-val cluster_ord =
-  prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
+fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
+  (ax_no, (cluster_no, (skolem, index_no)))
+fun cluster_ord p =
+  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
+           (pairself cluster_key p)
 
 val tysubst_ord =
   list_ord (prod_ord Term_Ord.fast_indexname_ord
@@ -792,10 +795,10 @@
         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
+      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
+      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        cat_lines (map string_for_subst_info substs))
-      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
-      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
 *)
       fun rotation_for_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs