store_standard_thm "norm_hhf_eq";

--- a/src/Pure/drule.ML	Fri Nov 10 19:08:30 2000 +0100
+++ b/src/Pure/drule.ML	Fri Nov 10 19:09:40 2000 +0100
@@ -615,7 +615,7 @@
         |> Thm.forall_intr cx
         |> Thm.implies_intr cphi
         |> Thm.implies_intr rhs)
-    |> standard |> curry Thm.name_thm "ProtoPure.norm_hhf_eq"
+    |> store_standard_thm "norm_hhf_eq"
   end;
 
 
@@ -828,7 +828,6 @@
 (*make an initial proof state, "PROP A ==> (PROP A)" *)
 fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
 
-
 end;