Quot/quotient_term.ML
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.
 *)