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)