--- a/Quot/quotient_typ.ML Wed Feb 17 09:26:38 2010 +0100
+++ b/Quot/quotient_typ.ML Wed Feb 17 09:27:02 2010 +0100
@@ -302,8 +302,8 @@
val _ = OuterKeyword.keyword "/"
val _ =
- OuterSyntax.local_theory_to_proof "quotient_type"
- "quotient type definitions (require equivalence proofs)"
- OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+ OuterSyntax.local_theory_to_proof "quotient_type"
+ "quotient type definitions (require equivalence proofs)"
+ OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
end; (* structure *)