src/Pure/Syntax/mixfix.ML
changeset 22709 9ab51bac6287
parent 22702 372da033ed93
child 22826 0f4c501a691e
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -154,8 +154,8 @@
     1.4    | mixfix_args (Binder _) = 1
     1.5    | mixfix_args Structure = 0;
     1.6  
     1.7 -fun mixfixT (Binder _) = (TypeInfer.logicT --> TypeInfer.logicT) --> TypeInfer.logicT
     1.8 -  | mixfixT mx = replicate (mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
     1.9 +fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
    1.10 +  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
    1.11  
    1.12  
    1.13  (* syn_ext_types *)