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/Syntax/mixfix.ML
changeset 22709 9ab51bac6287
parent 22702 372da033ed93
child 22826 0f4c501a691e 
--- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:49 2007 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:50 2007 +0200
@@ -154,8 +154,8 @@
   | 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;
+fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
+  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
 
 
 (* syn_ext_types *)
isabelle