--- 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