src/HOL/Tools/Metis/metis_reconstruct.ML

       THEN' (EVERY' (maps do_cluster_subst cluster_substs))
       THEN' rotate_tac (~ first_prem - length cluster_substs)
       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
                      (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
 

       fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
         "; 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
     in
       Goal.prove ctxt [] [] @{prop False}