Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_term.ML
changeset 1113 9f6c606d5b59
parent 1100 2fb07e01c57b
child 1128 17ca92ab4660 
--- 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 =
nominal2