# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266329551 -3600
# Node ID 6642df770bc41998ff33c1fa1679aa7a935bbd24
# Parent  a6fc645be6e2c69de2d114054c2b67d2eccd4a62
indenting

diff -r a6fc645be6e2 -r 6642df770bc4 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Mon Feb 15 17:02:46 2010 +0100
+++ b/Quot/quotient_typ.ML	Tue Feb 16 15:12:31 2010 +0100
@@ -277,9 +277,9 @@
     val rty = Syntax.read_typ lthy rty_str
     val lthy1 = Variable.declare_typ rty lthy
     val rel = 
-          Syntax.parse_term lthy1 rel_str
-          |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
-          |> Syntax.check_term lthy1 
+      Syntax.parse_term lthy1 rel_str
+      |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
+      |> Syntax.check_term lthy1 
     val lthy2 = Variable.declare_term rel lthy1
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)