--- a/src/HOL/Tools/Function/function_lib.ML Wed Apr 27 10:31:18 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Wed Apr 27 10:49:39 2011 +0200
@@ -23,8 +23,6 @@
val mk_forall_rename: (string * term) -> term -> term
val forall_intr_rename: (string * cterm) -> thm -> thm
- val frees_in_term: Proof.context -> term -> (string * typ) list
-
datatype proof_attempt = Solved of thm | Stuck of thm | Fail
val try_proof: cterm -> tactic -> proof_attempt
@@ -101,13 +99,6 @@
end
-(* Returns the frees in a term in canonical order, excluding the fixes from the context *)
-fun frees_in_term ctxt t =
- Term.add_frees t []
- |> filter_out (Variable.is_fixed ctxt o fst)
- |> rev
-
-
datatype proof_attempt = Solved of thm | Stuck of thm | Fail
fun try_proof cgoal tac =