# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266395209 -3600
# Node ID e860d8767d09b80a1a8346d5be0d2141f2316d94
# Parent  30fb2ca89773456210787c1eeedc7a28218f7463
indent

diff -r 30fb2ca89773 -r e860d8767d09 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Tue Feb 16 15:13:14 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Feb 17 09:26:49 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 *)