# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID 547a02d889f5ead7499f74830bec8e8273e02d83
# Parent  a4aeb26a63624720b5bff50c9bcab5673c125759
removed experimental code submitted by mistake

diff -r a4aeb26a6362 -r 547a02d889f5 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, [](*###*)), 0)
+                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
                                                   (Integer.add 1)) substs
         |> Int_Tysubst_Table.dest
       val needed_axiom_props =