# HG changeset patch
# User ballarin
# Date 1114500298 -7200
# Node ID 12b06f56209a95f2b593ce877ea93fcbbcad5826
# Parent  2aee4e5b792509a2742ce6a25941edf75452f456
Fixed bug in fact activation.

diff -r 2aee4e5b7925 -r 12b06f56209a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Apr 25 18:29:40 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Apr 26 09:24:58 2005 +0200
@@ -2052,7 +2052,7 @@
                 handle Option => error ("(internal) unknown registration of " ^
                   quote (fst id) ^ " while activating facts.")) all_elemss);
       in Library.foldl (activate_facts_elems get_reg note_thmss attrib
-        (Drule.standard o Drule.fconv_rule (Thm.beta_conversion true) o
+        (standard o Drule.fconv_rule (Thm.beta_conversion true) o
           Drule.satisfy_hyps prems)) (thy_ctxt, new_elemss) end;
 
 val global_activate_facts_elemss = gen_activate_facts_elemss