diff -r 64f9c76f70c7 -r 35436401f00d Quot/quotient_term.ML --- a/Quot/quotient_term.ML Sat Dec 26 23:20:46 2009 +0100 +++ b/Quot/quotient_term.ML Sun Dec 27 23:33:10 2009 +0100 @@ -402,6 +402,7 @@ regularize_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt + (*********************) (* Rep/Abs Injection *) (*********************) @@ -430,7 +431,7 @@ For free variables: - * We put aRep/Abs around it if the type needs lifting. + * We put a Rep/Abs around it if the type needs lifting. Vars case cannot occur. *)