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 1090 de2d1929899f
parent 1085 cf53861a00a7
child 1096 a69ec3f3f535
child 1097 551eacf071d7 
--- 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
nominal2