# HG changeset patch
# User berghofe
# Date 1004553125 -3600
# Node ID 402ae1a172aed66804bfd35fd2ec5042274dee36
# Parent  b409a8cbe1fb82ea4ab0e9a779e4cf1452a8151a
norm_hhf_eq is now stored using open_store_standard_thm.

diff -r b409a8cbe1fb -r 402ae1a172ae src/Pure/drule.ML
--- 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;