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.17 -   is_Var (head_of lhs)
    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