# HG changeset patch # User kuncar # Date 1323781460 -3600 # Node ID 67110d6c66dee6279c7328824015ee7d661dd797 # Parent ff7bdc67e8cb95c413e5819d57615cd3f6016f89 support phantom types as quotient types diff -r ff7bdc67e8cb -r 67110d6c66de src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Dec 12 23:06:41 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Dec 13 14:04:20 2011 +0100 @@ -65,7 +65,7 @@ | _ => raise Match) val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs - val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) + val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm)) val (_, prop') = Local_Defs.cert_def lthy prop val (_, newrhs) = Local_Defs.abs_def prop'