# HG changeset patch
# User wenzelm
# Date 1224189869 -7200
# Node ID 9846d772b30649488046fc570384f472106f6a05
# Parent  89f9dd800a228929af073e70e31d63f2ec1bdc3b
Drule.norm_hhf_eqs;

diff -r 89f9dd800a22 -r 9846d772b306 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu Oct 16 22:44:28 2008 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Oct 16 22:44:29 2008 +0200
@@ -193,7 +193,7 @@
 val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
 val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
 
-val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq));
+val _ = Context.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
 
 
 (* atomize *)
diff -r 89f9dd800a22 -r 9846d772b306 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Oct 16 22:44:28 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Oct 16 22:44:29 2008 +0200
@@ -1344,7 +1344,7 @@
   |> Thm.adjust_maxidx_thm ~1
   |> Drule.gen_all;
 
-val hhf_ss = empty_ss addsimps [Drule.norm_hhf_eq];
+val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 
 in