--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 19 19:34:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 20 10:58:01 2010 +0200
@@ -15,7 +15,6 @@
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
- val extensionalize_term : term -> term
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
@@ -101,25 +100,6 @@
Keyword.is_keyword s) ? quote
end
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Clausifier".) *)
-fun extensionalize_term t =
- let
- fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
- | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
- Type (_, [_, res_T])]))
- $ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name "op ="} orelse s = @{const_name "=="} then
- let val var_t = Var ((var_s, j), var_T) in
- Const (s, T' --> T' --> res_T)
- $ betapply (t2, var_t) $ subst_bound (var_t, t')
- |> aux (j + 1)
- end
- else
- t
- | aux _ t = t
- in aux (maxidx_of_term t + 1) t end
-
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>
case Type.lookup subst v of