author | nipkow |
Tue, 04 Nov 1997 12:59:01 +0100 | |
changeset 4117 | cf71befb65e8 |
parent 4116 | 42606637f87f |
child 4118 | 4e75435b01e5 |
--- a/src/HOL/simpdata.ML Tue Nov 04 12:58:10 1997 +0100 +++ b/src/HOL/simpdata.ML Tue Nov 04 12:59:01 1997 +0100 @@ -85,7 +85,7 @@ fun mk_meta_eq_simp r = case concl_of r of Const("==",_)$_$_ => r | _$(Const("op =",_)$lhs$rhs) => - (case fst(Logic.loops (#sign(rep_thm r)) (prems_of r) lhs rhs) of + (case fst(Logic.rewrite_rule_ok (#sign(rep_thm r)) (prems_of r) lhs rhs) of None => mk_meta_eq r | Some _ => r RS P_imp_P_eq_True) | _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False