norm_hhf_eq is now stored using open_store_standard_thm.

--- a/src/Pure/drule.ML	Wed Oct 31 01:28:39 2001 +0100
+++ b/src/Pure/drule.ML	Wed Oct 31 19:32:05 2001 +0100
@@ -661,7 +661,7 @@
         |> Thm.forall_intr cx
         |> Thm.implies_intr cphi
         |> Thm.implies_intr rhs)
-    |> store_standard_thm "norm_hhf_eq"
+    |> open_store_standard_thm "norm_hhf_eq"
   end;