changeset 797 | 35436401f00d |
parent 796 | 64f9c76f70c7 |
child 800 | 71225f4a4635 |
--- 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. *)