diff -r c7069b09730b -r 9f6c606d5b59 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Feb 10 10:55:14 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Feb 10 11:09:30 2010 +0100
@@ -90,7 +90,7 @@
       TVar _ => mk_Free rty
     | Type (_, []) => mk_identity rty
     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
-    | _ => raise LIFT_MATCH ("mk_mapfun (default)")
+    | _ => raise LIFT_MATCH "mk_mapfun (default)"
 in
   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
@@ -706,7 +706,7 @@
       | x => x)
 
 (* subst_trms takes a list of (rtrm, qtrm) substitution pairs
-   and if the  given term matches any of the raw terms it
+   and if the given term matches any of the raw terms it
    returns the appropriate qtrm instantiated. If none of
    them matched it returns NONE. *)
 fun subst_trm thy t (rtrm, qtrm) s =