# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266249249 -3600
# Node ID a0e6d6b54509ea6d30b4a5984a241f4207983a2f
# Parent  7763756b42cffc4c42bcf32d00bca59baeaf59a3# Parent  368ec514aa34f37b3f5da460cf6def32576fdfb2
merge

diff -r 7763756b42cf -r a0e6d6b54509 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Mon Feb 15 16:53:51 2010 +0100
+++ b/Quot/quotient_typ.ML	Mon Feb 15 16:54:09 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 "/"