find_tname now handles parameter renaming properly ("as they are printed").
authorberghofe
Wed, 25 Feb 2004 15:17:24 +0100
changeset 14412 109cc0dc706b
parent 14411 7851e526b8b7
child 14413 7ce47ab455eb
find_tname now handles parameter renaming properly ("as they are printed").
src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Feb 24 16:38:51 2004 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Feb 25 15:17:24 2004 +0100
@@ -143,7 +143,7 @@
 
 fun find_tname var Bi =
   let val frees = map dest_Free (term_frees Bi)
-      val params = Logic.strip_params Bi;
+      val params = rename_wrt_term Bi (Logic.strip_params Bi);
   in case assoc (frees @ params, var) of
        None => error ("No such variable in subgoal: " ^ quote var)
      | Some(Type (tn, _)) => tn