# HG changeset patch
# User nipkow
# Date 864202161 -7200
# Node ID 8358e19d0d4cdcaf2c7a238d2f52ad398d78e48f
# Parent  4ca0b6507ed5eb02f169289a87e81813f6702ef3
Replaced Konrad's own add_term_names by the predefined one.
Replaced fn Free x => x by dest_Free.

diff -r 4ca0b6507ed5 -r 8358e19d0d4c src/HOL/datatype.ML
--- 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)
diff -r 4ca0b6507ed5 -r 8358e19d0d4c src/HOL/thy_data.ML
--- 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)