Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced check_term o parse_term by read_term
authorChristian Urban <urbanc@in.tum.de>
Thu, 05 Nov 2009 10:23:27 +0100
changeset 287 fc72f5b2f9d7
parent 286 a031bcaf6719
child 288 f1a840dd0743
replaced check_term o parse_term by read_term
quotient_def.ML file | annotate | diff | comparison | revisions 
--- 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
nominal2