src/HOL/Tools/BNF/bnf_util.ML

 
 
 (** Types **)
 
 (*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*)
-fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
-    1 + num_binder_types T2
-  | num_binder_types _ = 0
+fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T
+  | num_binder_types _ = 0;
 
 (*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*)
 fun strip_typeN 0 T = ([], T)
   | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
   | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []);

   let val ((AT, BT), FT) = `dest_funT (fastype_of f);
   in Const (@{const_name Grp}, HOLogic.mk_setT AT --> FT --> mk_pred2T AT BT) $ A $ f end;
 
 fun mk_image f =
   let val (T, U) = dest_funT (fastype_of f);
-  in Const (@{const_name image},
-    (T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end;
+  in Const (@{const_name image}, (T --> U) --> HOLogic.mk_setT T --> HOLogic.mk_setT U) $ f end;
 
 fun mk_Ball X f =
   Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
 
 fun mk_Bex X f =

   in
     Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
       mk_Field bd $ bd
   end;
 
-fun mk_cinfinite bd =
-  Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
+fun mk_cinfinite bd = Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
 
 fun mk_ordLeq t1 t2 =
   HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
     Const (@{const_name ordLeq}, mk_relT (fastype_of t1, fastype_of t2)));
 

 
 fun mk_card_binop binop typop t1 t2 =
   let
     val (T1, relT1) = `(fst o dest_relT) (fastype_of t1);
     val (T2, relT2) = `(fst o dest_relT) (fastype_of t2);
-  in
-    Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2
-  end;
+  in Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2 end;
 
 val mk_csum = mk_card_binop @{const_name csum} mk_sumT;
 val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT;
 val mk_cexp = mk_card_binop @{const_name cexp} (op --> o swap);
 val ctwo = @{term ctwo};