changeset 13743 | f8f9393be64c |
parent 13600 | 9702c8636a7b |
child 14430 | 5cb24165a2e1 |
--- a/src/HOL/simpdata.ML Fri Dec 06 15:16:30 2002 +0100 +++ b/src/HOL/simpdata.ML Mon Dec 09 10:38:56 2002 +0100 @@ -151,7 +151,7 @@ (*Congruence rules for = (instead of ==)*) fun mk_meta_cong rl = - standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) + zero_var_indexes(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) handle THM _ => error("Premises and conclusion of congruence rules must be =-equalities");