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