Mercurial Mercurial > repos > isabelle / 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.
added mixfixT (from type_infer.ML);
authorwenzelm
Sun, 15 Apr 2007 14:32:02 +0200
changeset 22702 372da033ed93
parent 22701 4346f230283d
child 22703 d9fbdfe22543
added mixfixT (from type_infer.ML);
src/Pure/Syntax/mixfix.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 14:32:01 2007 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 14:32:02 2007 +0200
@@ -33,6 +33,7 @@
   val const_mixfix: string -> mixfix -> string * mixfix
   val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
+  val mixfixT: mixfix -> typ
 end;
 
 signature MIXFIX =
@@ -153,6 +154,9 @@
   | mixfix_args (Binder _) = 1
   | mixfix_args Structure = 0;
 
+fun mixfixT (Binder _) = (TypeInfer.logicT --> TypeInfer.logicT) --> TypeInfer.logicT
+  | mixfixT mx = replicate (mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
+
 
 (* syn_ext_types *)
isabelle