1419 raise SIMPLIFIER("Rewrite rule not a meta-equality",thm) |
1419 raise SIMPLIFIER("Rewrite rule not a meta-equality",thm) |
1420 val econcl = Pattern.eta_contract concl |
1420 val econcl = Pattern.eta_contract concl |
1421 val (elhs,erhs) = Logic.dest_equals econcl |
1421 val (elhs,erhs) = Logic.dest_equals econcl |
1422 val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) |
1422 val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) |
1423 andalso not(is_Var(elhs)) |
1423 andalso not(is_Var(elhs)) |
1424 in |
1424 in if not(term_vars(erhs) subset |
1425 if not perm andalso loops sign prems (elhs,erhs) then |
1425 (term_vars(elhs) union flat(map term_vars prems))) |
1426 (prtm_warning "ignoring looping rewrite rule" sign prop; None) |
1426 then (prtm_warning "extra Var(s) on rhs" sign prop; None) else |
|
1427 if not perm andalso loops sign prems (elhs,erhs) |
|
1428 then (prtm_warning "ignoring looping rewrite rule" sign prop; None) |
1427 else Some{thm=thm,lhs=lhs,perm=perm} |
1429 else Some{thm=thm,lhs=lhs,perm=perm} |
1428 end; |
1430 end; |
1429 |
1431 |
1430 local |
1432 local |
1431 fun eq({thm=Thm{prop=p1,...},...}:rrule, |
1433 fun eq({thm=Thm{prop=p1,...},...}:rrule, |