# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257413007 -3600
# Node ID fc72f5b2f9d7faddebd185ee362b0ea6a30c5776
# Parent  a031bcaf6719b8ceab4d36dcc332fd3a6896e0f2
replaced check_term o parse_term by read_term

diff -r a031bcaf6719 -r fc72f5b2f9d7 quotient_def.ML
--- a/quotient_def.ML	Thu Nov 05 09:55:21 2009 +0100
+++ b/quotient_def.ML	Thu Nov 05 10:23:27 2009 +0100
@@ -163,8 +163,8 @@
 
 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 
 let
-  val qty  = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
-  val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
+  val qty  = Syntax.read_typ lthy qtystr
+  val prop = Syntax.read_prop lthy propstr
 in
   quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
 end