--- a/src/HOL/Orderings.thy Wed Feb 21 02:30:06 2007 +0100
+++ b/src/HOL/Orderings.thy Wed Feb 21 13:51:12 2007 +0100
@@ -534,19 +534,20 @@
((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
- fun mk v v' c n P =
- if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
- then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
+ fun matches_bound v t =
+ case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
+ | _ => false
+ fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
+ fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P
fun tr' q = (q,
fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
(case AList.lookup (op =) trans (q, c, d) of
NONE => raise Match
| SOME (l, g) =>
- (case (t, u) of
- (Const ("_bound", _) $ Free (v', _), n) => mk v v' l n P
- | (n, Const ("_bound", _) $ Free (v', _)) => mk v v' g n P
- | _ => raise Match))
+ if matches_bound v t andalso not (contains_var v u) then mk v l u P
+ else if matches_bound v u andalso not (contains_var v t) then mk v g t P
+ else raise Match)
| _ => raise Match);
in [tr' All_binder, tr' Ex_binder] end
*}