# HG changeset patch
# User wenzelm
# Date 973879780 -3600
# Node ID d727c39c4a4b102df143e1a1ff28074c855eccda
# Parent  2074e62da3548a096c19ed325fb3fb2881843ce4
store_standard_thm "norm_hhf_eq";

diff -r 2074e62da354 -r d727c39c4a4b src/Pure/drule.ML
--- 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;