# HG changeset patch
# User blanchet
# Date 1357332979 -3600
# Node ID 7ce87037fbeba049222ba30637c55b2b14a73704
# Parent  b2e7490a1b3d4a4b909709e93302ab336476446b
tuning

diff -r b2e7490a1b3d -r 7ce87037fbeb src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 04 21:56:19 2013 +0100
@@ -331,15 +331,13 @@
   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
 
 fun build_all_names name_of facts =
-  Termtab.fold
-      (fn (_, aliases as main :: _) =>
-          fold (fn alias =>
-                   Symtab.update (name_of alias,
-                                  name_of (if_thm_before main alias))) aliases)
-      (fold_rev (fn (_, thm) =>
-                    Termtab.cons_list (normalize_eq_etc (prop_of thm), thm))
-            facts Termtab.empty)
-      Symtab.empty
+  let
+    fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
+    fun add_alias canon alias =
+      Symtab.update (name_of alias, name_of (if_thm_before canon alias))
+    fun add_aliases (_, aliases as canon :: _) = fold (add_alias canon) aliases
+    val tab = fold_rev cons_thm facts Termtab.empty
+  in Termtab.fold add_aliases tab Symtab.empty end
 
 fun uniquify facts =
   Termtab.fold (cons o snd)