Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/simpdata.ML
changeset 4117 cf71befb65e8
parent 4086 958806f7e840
child 4119 de6e388f3d86 
--- 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
isabelle