src/Pure/goal.ML

   val init: cterm -> thm
   val protect: thm -> thm
   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
   val prove_multi: theory -> string list -> term list -> term list ->
     (thm list -> tactic) -> thm list

     addsimps [Drule.norm_hhf_eq];
 
 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;
 
 
 (* composition of normal results *)