| changeset 17203 | 29b2563f5c11 |
| parent 16983 | c895701d55ea |
| child 17325 | d9d50222808e |
--- a/src/Pure/drule.ML Wed Aug 31 15:46:39 2005 +0200 +++ b/src/Pure/drule.ML Wed Aug 31 15:46:40 2005 +0200 @@ -852,7 +852,7 @@ 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 ****)