src/Pure/thm.ML
 changeset 3893 5a1f22e7b359 parent 3812 66fa30839377 child 3895 b2463861c86a
```     1.1 --- a/src/Pure/thm.ML	Thu Oct 16 13:43:42 1997 +0200
1.2 +++ b/src/Pure/thm.ML	Thu Oct 16 13:45:16 1997 +0200
1.3 @@ -1535,44 +1535,16 @@
1.4
1.5  (* mk_rrule *)
1.6
1.7 -fun vperm (Var _, Var _) = true
1.8 -  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
1.9 -  | vperm (t1 \$ t2, u1 \$ u2) = vperm (t1, u1) andalso vperm (t2, u2)
1.10 -  | vperm (t, u) = (t = u);
1.11 -
1.12 -fun var_perm (t, u) =
1.13 -  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
1.14 -
1.15 -(*simple test for looping rewrite*)
1.16 -fun loops sign prems (lhs, rhs) =
1.18 -  orelse
1.19 -   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
1.20 -  orelse
1.21 -   (null prems andalso
1.22 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
1.23 -(*the condition "null prems" in the last case is necessary because
1.24 -  conditional rewrites with extra variables in the conditions may terminate
1.25 -  although the rhs is an instance of the lhs. Example:
1.26 -  ?m < ?n ==> f(?n) == f(?m)*)
1.27 -
1.28  fun mk_rrule (thm as Thm {sign, prop, ...}) =
1.29    let
1.30      val prems = Logic.strip_imp_prems prop;
1.31      val concl = Logic.strip_imp_concl prop;
1.32 -    val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
1.33 +    val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
1.34        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
1.35 -    val econcl = Pattern.eta_contract concl;
1.36 -    val (elhs, erhs) = Logic.dest_equals econcl;
1.37 -    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
1.38 -      andalso not (is_Var elhs);
1.39 -  in
1.40 -    if not ((term_vars erhs) subset
1.41 -        (union_term (term_vars elhs, List.concat(map term_vars prems)))) then
1.42 -      (prtm_warning "extra Var(s) on rhs" sign prop; None)
1.43 -    else if not perm andalso loops sign prems (elhs, erhs) then
1.44 -      (prtm_warning "ignoring looping rewrite rule" sign prop; None)
1.45 -    else Some {thm = thm, lhs = lhs, perm = perm}
1.46 +  in case Logic.loops sign prems lhs rhs of
1.47 +     (None,perm) => Some {thm = thm, lhs = lhs, perm = perm}
1.48 +   | (Some msg,_) =>
1.49 +        (prtm_warning("ignoring rewrite rule ("^msg^")") sign prop; None)
1.50    end;
1.51
1.52
```