# HG changeset patch
# User blanchet
# Date 1357857260 -3600
# Node ID 41b804049fae7d1c1aecaa07431efa986acf9736
# Parent  4247cbd78aaf3f9ca3eda559404a38916faa0c3a
make name table work the way it was intended to

diff -r 4247cbd78aaf -r 41b804049fae src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 10 23:34:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 10 23:34:20 2013 +0100
@@ -344,12 +344,12 @@
   let
     fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
     fun add_plain canon alias =
-      Symtab.update (Thm.get_name_hint canon,
+      Symtab.update (Thm.get_name_hint alias,
                      name_of (if_thm_before canon alias))
     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
     fun add_inclass (name, target) =
       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
-    val prop_tab = fold_rev cons_thm facts Termtab.empty
+    val prop_tab = fold cons_thm facts Termtab.empty
     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   in (plain_name_tab, inclass_name_tab) end