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 1096 a69ec3f3f535
parent 1094 6961fda38e09
parent 1090 de2d1929899f
child 1098 f64d826a3f55 
--- a/Quot/quotient_term.ML	Tue Feb 09 15:20:40 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 15:20:52 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
nominal2