# HG changeset patch
# User haftmann
# Date 1232349403 -3600
# Node ID fe9cfe076c23fcb27604da83a602d62c5ea883a2
# Parent  9846af6c6d6a42ded603060fd45bb4a618595cfa
tuned

diff -r 9846af6c6d6a -r fe9cfe076c23 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Jan 19 08:16:42 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Jan 19 08:16:43 2009 +0100
@@ -806,15 +806,15 @@
 
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     
-    fun store_dep ((name, morph), thms) =
+    fun store_dep (name, morph) thms =
       Locale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
 
     fun after_qed results =
       ProofContext.theory (
         (* store dependencies *)
-        fold store_dep (deps ~~ prep_result propss results) #>
+        fold2 store_dep deps (prep_result propss results) #>
         (* propagate registrations *)
-        (fn thy => fold_rev (fn reg => Locale.activate_global_facts reg)
+        (fn thy => fold_rev Locale.activate_global_facts
           (Locale.get_registrations thy) thy));
   in
     goal_ctxt |>