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