--- a/src/HOL/Tools/TFL/rules.ML Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Mon Jul 06 21:24:30 2009 +0200
@@ -519,14 +519,14 @@
handle TERM _ => get (rst, n+1, L)
| U.ERR _ => get (rst, n+1, L);
-(* Note: rename_params_rule counts from 1, not 0 *)
+(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
let val thy = Thm.theory_of_thm thm
val tych = cterm_of thy
val ants = Logic.strip_imp_prems (Thm.prop_of thm)
val news = get (ants,1,[])
in
- fold rename_params_rule news thm
+ fold Thm.rename_params_rule news thm
end;