src/HOL/Tools/datatype_package.ML
changeset 14412 109cc0dc706b
parent 14174 f3cafd2929d5
child 14471 5688b05b2575
     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