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.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 17 Feb 2010 09:26:38 +0100
changeset 1165 f1253f280843
parent 1164 fe0a31cf30a0 (current diff)
parent 1163 30fb2ca89773 (diff)
child 1167 e09d148ccc94
merge
--- a/Quot/quotient_typ.ML	Wed Feb 17 09:26:10 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Feb 17 09:26:38 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)
nominal2