1.1 --- a/src/HOL/Orderings.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -727,8 +727,8 @@
     1.4    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
     1.5    fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P;
     1.6  
     1.7 -  fun tr' q = (q,
     1.8 -    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
     1.9 +  fun tr' q = (q, fn _ =>
    1.10 +    (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
    1.11          Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    1.12          (case AList.lookup (op =) trans (q, c, d) of
    1.13            NONE => raise Match
    1.14 @@ -736,7 +736,7 @@
    1.15              if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
    1.16              else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P
    1.17              else raise Match)
    1.18 -     | _ => raise Match);
    1.19 +      | _ => raise Match));
    1.20  in [tr' All_binder, tr' Ex_binder] end
    1.21  *}
    1.22