diff -r 66097fe4942a -r de2d1929899f Quot/quotient_term.ML
--- 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