src/Pure/drule.ML

       | is_norm _ = true;
   in is_norm (Pattern.beta_eta_contract tm) end;
 
 fun norm_hhf thy t =
   if is_norm_hhf t then t
-  else Pattern.rewrite_term (Sign.tsig_of thy) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
+  else Pattern.rewrite_term thy [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
 
 
 (*** Instantiate theorem th, reading instantiations in theory thy ****)
 
 (*Version that normalizes the result: Thm.instantiate no longer does that*)