# HG changeset patch
# User wenzelm
# Date 1132941518 -3600
# Node ID 9e2c15ae0e86989e551b2d51891243a8d8db4533
# Parent  552bbf45233e856980680d5f7037e4d080d62091
tuned names;

diff -r 552bbf45233e -r 9e2c15ae0e86 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Nov 25 18:58:37 2005 +0100
+++ b/src/Pure/goal.ML	Fri Nov 25 18:58:38 2005 +0100
@@ -18,7 +18,7 @@
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_hhf: thm -> thm
-  val norm_hhf_protected: thm -> thm
+  val norm_hhf_protect: thm -> thm
   val compose_hhf: thm -> int -> thm -> thm Seq.seq
   val compose_hhf_tac: thm -> int -> tactic
   val comp_hhf: thm -> thm -> thm
@@ -90,7 +90,7 @@
 in
 
 val norm_hhf = gen_norm_hhf ss;
-val norm_hhf_protected = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
+val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
 
 end;