Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 43262 547a02d889f5
parent 43259 30c141dc22d6
child 43268 c0eaa8b9bff5 
--- 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 =
isabelle