diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -706,7 +706,7 @@
       val ax_counts =
         Int_Tysubst_Table.empty
         |> fold (fn (ax_no, (_, (tysubst, _))) =>
-                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
+                    Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0)
                                                   (Integer.add 1)) substs
         |> Int_Tysubst_Table.dest
       val needed_axiom_props =