diff -r 44461d5615eb -r f4da25147389 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Feb 06 10:04:56 2010 +0100
+++ b/Quot/quotient_term.ML	Sat Feb 06 12:58:56 2010 +0100
@@ -714,10 +714,10 @@
         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
       | x => x)
 
-fun subst_trm thy t (rt, qt) s =
+fun subst_trm thy t (rtrm, qtrm) s =
   if s <> NONE then s else
-    case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of
-      SOME inst => SOME (Envir.subst_term inst qt)
+    case try (Pattern.match thy (t, rtrm)) (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