src/Pure/tactic.ML

   val metacut_tac       : thm -> int -> tactic
   val net_bimatch_tac   : (bool*thm) list -> int -> tactic
   val net_biresolve_tac : (bool*thm) list -> int -> tactic
   val net_match_tac     : thm list -> int -> tactic
   val net_resolve_tac   : thm list -> int -> tactic
+  val norm_hhf_plain    : thm -> thm
   val norm_hhf_rule     : thm -> thm
   val norm_hhf_tac      : int -> tactic
   val prune_params_tac  : tactic
   val rename_params_tac : string list -> int -> tactic
   val rename_tac        : string -> int -> tactic

 
 (*Rewrite subgoals only, not main goal. *)
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 fun rewtac def = rewrite_goals_tac [def];
 
+fun norm_hhf_plain th =
+  if Drule.is_norm_hhf (prop_of th) then th
+  else rewrite_rule [Drule.norm_hhf_eq] th;
+
 fun norm_hhf_rule th =
- (if Drule.is_norm_hhf (prop_of th) then th
-  else rewrite_rule [Drule.norm_hhf_eq] th) |> Drule.gen_all;
+  th |> norm_hhf_plain |> Drule.gen_all;
 
 val norm_hhf_tac =
   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   THEN' SUBGOAL (fn (t, i) =>
     if Drule.is_norm_hhf t then all_tac