src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

     val (premises, head) = Logic.strip_horn intro
   in
     Logic.list_implies (maps f premises, head)
   end
 
+fun map_concl f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (premises, f head)
+  end
+
+(* combinators to apply a function to all basic parts of nested products *)
+
+fun map_products f (Const ("Pair", T) $ t1 $ t2) =
+  Const ("Pair", T) $ map_products f t1 $ map_products f t2
+  | map_products f t = f t
 
 (* split theorems of case expressions *)
 
 (*
 fun has_split_rule_cname @{const_name "nat_case"} = true

     val intro''''' = map_term thy (maps_premises split_conj) intro''''
   in
     intro'''''
   end
 
+(* eta contract higher-order arguments *)
+
+
+fun eta_contract_ho_arguments thy intro =
+  let
+    fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom))
+  in
+    map_term thy (map_concl f o map_atoms f) intro
+  end
+
+
 end;