Drule.norm_hhf_eqs;
authorwenzelm
Thu, 16 Oct 2008 22:44:29 +0200
changeset 28620 9846d772b306
parent 28619 89f9dd800a22
child 28621 a60164e8fff0
Drule.norm_hhf_eqs;
src/Pure/Isar/object_logic.ML
src/Pure/meta_simplifier.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 *)
--- 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