src/HOL/Tools/Nitpick/nitpick_util.ML

   val plural_s_for_list : 'a list -> string
   val serial_commas : string -> string list -> string list
   val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
+  val nat_subscript : int -> string
   val flip_polarity : polarity -> polarity
   val prop_T : typ
   val bool_T : typ
   val nat_T : typ
   val int_T : typ

   val is_of_class_const : theory -> string * typ -> bool
   val get_class_def : theory -> string -> (string * term) option
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> string * typ -> term -> term
   val varify_type : Proof.context -> typ -> typ
-  val nat_subscript : int -> string
+  val eta_expand : typ list -> term -> int -> term
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
   val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
   val indent_size : int
   val pstrs : string -> Pretty.T list

     p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps
 
 val parse_bool_option = Sledgehammer_Util.parse_bool_option
 val parse_time_option = Sledgehammer_Util.parse_time_option
 
-fun flip_polarity Pos = Neg
-  | flip_polarity Neg = Pos
-  | flip_polarity Neut = Neut
-
-val prop_T = @{typ prop}
-val bool_T = @{typ bool}
-val nat_T = @{typ nat}
-val int_T = @{typ int}
-
-val simple_string_of_typ = Refute.string_of_typ
-val is_real_constr = Refute.is_IDT_constructor
-val typ_of_dtyp = Refute.typ_of_dtyp
-val is_of_class_const = Refute.is_const_of_class
-val get_class_def = Refute.get_classdef
-val monomorphic_term = Sledgehammer_Util.monomorphic_term
-val specialize_type = Sledgehammer_Util.specialize_type
-
-fun varify_type ctxt T =
-  Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
-  |> snd |> the_single |> dest_Const |> snd
-
 val i_subscript = implode o map (prefix "\<^isub>") o explode
 fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
 fun nat_subscript n =
   let val s = signed_string_of_int n in
     if print_mode_active Symbol.xsymbolsN then

       (if n <= 9 then be_subscript else i_subscript) s
     else
       s
   end
 
+fun flip_polarity Pos = Neg
+  | flip_polarity Neg = Pos
+  | flip_polarity Neut = Neut
+
+val prop_T = @{typ prop}
+val bool_T = @{typ bool}
+val nat_T = @{typ nat}
+val int_T = @{typ int}
+
+val simple_string_of_typ = Refute.string_of_typ
+val is_real_constr = Refute.is_IDT_constructor
+val typ_of_dtyp = Refute.typ_of_dtyp
+val is_of_class_const = Refute.is_const_of_class
+val get_class_def = Refute.get_classdef
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
+
+fun varify_type ctxt T =
+  Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
+  |> snd |> the_single |> dest_Const |> snd
+
+val eta_expand = Sledgehammer_Util.eta_expand
+
 fun time_limit NONE = I
   | time_limit (SOME delay) = TimeLimit.timeLimit delay
 
 fun DETERM_TIMEOUT delay tac st =
   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))