Replaced Konrad's own add_term_names by the predefined one.
Replaced fn Free x => x by dest_Free.
--- a/src/HOL/datatype.ML Tue May 20 19:57:12 1997 +0200
+++ b/src/HOL/datatype.ML Wed May 21 10:09:21 1997 +0200
@@ -639,7 +639,7 @@
(*---------------------------------------------------------------------------
* Names of all variables occurring in a term, including bound ones. These
* are added into the second argument.
- *---------------------------------------------------------------------------*)
+ *---------------------------------------------------------------------------
fun add_term_names tm =
let fun insert (x:string) =
let fun canfind[] = [x]
@@ -655,7 +655,8 @@
| add _ V = V
in add tm
end;
-
+Why bound ones???
+*)
(*---------------------------------------------------------------------------
* We need to make everything free, so that we can put the term into a
@@ -693,7 +694,7 @@
val clause1 = hd clauses
val left = (#1 o dest_eq) clause1
val ty = type_of ((#2 o dest_comb) left)
- val varnames = itlist add_term_names clauses []
+ val varnames = foldr add_term_names (clauses, [])
val M = variant varnames "M"
val Mvar = Free(M, ty)
val M' = variant (M::varnames) M
@@ -755,7 +756,7 @@
fun build_nchotomy sign case_rewrites =
let val clauses = map concl case_rewrites
val C_ybars = map (rand o #1 o dest_eq) clauses
- val varnames = itlist add_term_names C_ybars []
+ val varnames = foldr add_term_names (C_ybars, [])
val vname = variant varnames "v"
val ty = type_of (hd C_ybars)
val v = mk_var(vname,ty)
--- a/src/HOL/thy_data.ML Tue May 20 19:57:12 1997 +0200
+++ b/src/HOL/thy_data.ML Wed May 21 10:09:21 1997 +0200
@@ -52,7 +52,7 @@
(* generic induction tactic for datatypes *)
fun induct_tac var i =
let fun find_tname Bi =
- let val frees = map (fn Free x => x) (term_frees Bi)
+ let val frees = map dest_Free (term_frees Bi)
val params = Logic.strip_params Bi;
in case assoc (frees@params, var) of
None => error("No such variable in subgoal: " ^ quote var)