# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266249152 -3600
# Node ID 368ec514aa34f37b3f5da460cf6def32576fdfb2
# Parent  fbaebf08c1bd6717b256b2e305bce24c498a1e2a# Parent  2ad8e66de294b85cd4f59eeade71139daafe02d7
merge

diff -r 2ad8e66de294 -r 368ec514aa34 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Mon Feb 15 16:51:30 2010 +0100
+++ b/Quot/quotient_typ.ML	Mon Feb 15 16:52:32 2010 +0100
@@ -276,14 +276,11 @@
     (* new parsing with proper declaration *)
     val rty = Syntax.read_typ lthy rty_str
     val lthy1 = Variable.declare_typ rty lthy
-    val pre_rel = Syntax.parse_term lthy1 rel_str
-    val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
-    val rel = Syntax.check_term lthy1 pre_rel'
+    val rel = 
+          Syntax.parse_term lthy1 rel_str
+          |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
+          |> Syntax.check_term lthy1 
     val lthy2 = Variable.declare_term rel lthy1
-
-    (* old parsing *)
-    (* val rty = Syntax.read_typ lthy rty_str
-       val rel = Syntax.read_term lthy rel_str *)
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)
   end
@@ -293,11 +290,14 @@
   quotient_type spec' lthy'
 end
 
+local
+  structure P = OuterParse;
+in
+
 val quotspec_parser =
-    OuterParse.and_list1
-     ((OuterParse.type_args -- OuterParse.binding) --
-        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
-         (OuterParse.$$$ "/" |-- OuterParse.term))
+    P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- 
+       (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term))
+end
 
 val _ = OuterKeyword.keyword "/"