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