| changeset 13198 | 3e40f48a500f |
| parent 13105 | 3d1e7a199bdc |
| child 13325 | 5b5e12f0aee0 |
--- a/src/Pure/drule.ML Fri May 31 18:49:31 2002 +0200 +++ b/src/Pure/drule.ML Fri May 31 18:50:03 2002 +0200 @@ -705,7 +705,7 @@ fun norm_hhf sg t = if is_norm_hhf t then t - else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] t; + else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t; (*** Instantiate theorem th, reading instantiations under signature sg ****)