--- a/Quot/Nominal/Abs.thy	Mon Feb 08 13:50:52 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 09 10:48:42 2010 +0100
@@ -226,7 +226,6 @@
 
 (* TEST case *)
 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
-
 thm abs_induct abs_induct2
 
 instantiation abs :: (pt) pt

--- a/Quot/quotient_term.ML	Mon Feb 08 13:50:52 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 10:48:42 2010 +0100
@@ -694,7 +694,7 @@
    by appropriate qty, with substitution *)
 fun subst_ty thy ty (rty, qty) r =
   if r <> NONE then r else
-  case try (Sign.typ_match thy (ty, rty)) Vartab.empty of
+  case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
     SOME inst => SOME (Envir.subst_type inst qty)
   | NONE => NONE
 fun subst_tys thy substs ty =
@@ -711,7 +711,7 @@
    them matched it returns NONE. *)
 fun subst_trm thy t (rtrm, qtrm) s =
   if s <> NONE then s else
-    case try (Pattern.match thy (t, rtrm)) (Vartab.empty, Vartab.empty) of
+    case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
       SOME inst => SOME (Envir.subst_term inst qtrm)
     | NONE => NONE;
 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE