# HG changeset patch # User Cezary Kaliszyk # Date 1265708922 -3600 # Node ID de2d1929899fd01e6ebd9b61dd366a3b64bbab88 # Parent 66097fe4942a0fb66f7d503d66e7f9d94916ed71 Fixed pattern matching, now the test in Abs works correctly. diff -r 66097fe4942a -r de2d1929899f Quot/Nominal/Abs.thy --- a/Quot/Nominal/Abs.thy Mon Feb 08 13:50:52 2010 +0100 +++ b/Quot/Nominal/Abs.thy Tue Feb 09 10:48:42 2010 +0100 @@ -226,7 +226,6 @@ (* TEST case *) lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted] - thm abs_induct abs_induct2 instantiation abs :: (pt) pt diff -r 66097fe4942a -r de2d1929899f Quot/quotient_term.ML --- 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