tuned names;
authorwenzelm
Fri Nov 25 18:58:38 2005 +0100 (2005-11-25)
changeset 182529e2c15ae0e86
parent 18251 552bbf45233e
child 18253 0626a0a217ec
tuned names;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Fri Nov 25 18:58:37 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Fri Nov 25 18:58:38 2005 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_hhf: thm -> thm
     1.7 -  val norm_hhf_protected: thm -> thm
     1.8 +  val norm_hhf_protect: thm -> thm
     1.9    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    1.10    val compose_hhf_tac: thm -> int -> tactic
    1.11    val comp_hhf: thm -> thm -> thm
    1.12 @@ -90,7 +90,7 @@
    1.13  in
    1.14  
    1.15  val norm_hhf = gen_norm_hhf ss;
    1.16 -val norm_hhf_protected = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
    1.17 +val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
    1.18  
    1.19  end;
    1.20