# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266395222 -3600
# Node ID e09d148ccc9420cad6c70e49c7b64049a1301a38
# Parent  e860d8767d09b80a1a8346d5be0d2141f2316d94# Parent  f1253f28084389ca6c8a595d8da39ba30c687f5a
merge

diff -r f1253f280843 -r e09d148ccc94 Quot/quotient_typ.ML
--- 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 *)