Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/consts.ML
changeset 29581 b3b33e0298eb
parent 29251 8f84a608883d
child 29606 fedb8be05f24 
--- a/src/Pure/consts.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/consts.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -30,10 +30,10 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
+  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
-    Binding.T * term -> T -> (term * term) * T
+    binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
   val empty: T
isabelle