# HG changeset patch
# User berghofe
# Date 1077718644 -3600
# Node ID 109cc0dc706b0fde8010082236d045553d1dd790
# Parent  7851e526b8b7634d452cbe011573347aee0d3a04
find_tname now handles parameter renaming properly ("as they are printed").

diff -r 7851e526b8b7 -r 109cc0dc706b 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