Changed interface of Pattern.rewrite_term.
authorberghofe
Fri May 31 18:50:03 2002 +0200 (2002-05-31)
changeset 131983e40f48a500f
parent 13197 0567f4fd1415
child 13199 18402c1f76bf
Changed interface of Pattern.rewrite_term.
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri May 31 18:49:31 2002 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri May 31 18:50:03 2002 +0200
     1.3 @@ -247,7 +247,7 @@
     1.4        null (foldr add_term_consts (map fst ps, []) inter cnames))
     1.5          (Symtab.dest (thms_of_proof Symtab.empty prf))) \\ defnames
     1.6    in
     1.7 -    rewrite_terms (Pattern.rewrite_term tsig defs') (insert_refl defnames []
     1.8 +    rewrite_terms (Pattern.rewrite_term tsig defs' []) (insert_refl defnames []
     1.9        (Reconstruct.expand_proof sign thmnames prf))
    1.10    end;
    1.11  
     2.1 --- a/src/Pure/drule.ML	Fri May 31 18:49:31 2002 +0200
     2.2 +++ b/src/Pure/drule.ML	Fri May 31 18:50:03 2002 +0200
     2.3 @@ -705,7 +705,7 @@
     2.4  
     2.5  fun norm_hhf sg t =
     2.6    if is_norm_hhf t then t
     2.7 -  else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] t;
     2.8 +  else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
     2.9  
    2.10  
    2.11  (*** Instantiate theorem th, reading instantiations under signature sg ****)