src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 38652 e063be321438
parent 38284 9f98107ad8b4
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 14:51:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 14:54:17 2010 +0200
     1.3 @@ -141,7 +141,6 @@
     1.4      hol_context -> bool -> styp -> int -> styp
     1.5    val sel_no_from_name : string -> int
     1.6    val close_form : term -> term
     1.7 -  val eta_expand : typ list -> term -> int -> term
     1.8    val distinctness_formula : typ -> term list -> term
     1.9    val register_frac_type :
    1.10      string -> (string * string) list -> morphism -> Context.generic
    1.11 @@ -919,14 +918,6 @@
    1.12        | aux zs t = close_up zs (Term.add_vars t zs) t
    1.13    in aux [] end
    1.14  
    1.15 -fun eta_expand _ t 0 = t
    1.16 -  | eta_expand Ts (Abs (s, T, t')) n =
    1.17 -    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
    1.18 -  | eta_expand Ts t n =
    1.19 -    fold_rev (curry3 Abs ("x" ^ nat_subscript n))
    1.20 -             (List.take (binder_types (fastype_of1 (Ts, t)), n))
    1.21 -             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
    1.22 -
    1.23  fun distinctness_formula T =
    1.24    all_distinct_unordered_pairs_of
    1.25    #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))