src/Tools/induct.ML
changeset 29276 94b1ffec9201
parent 28965 1de908189869
child 29581 b3b33e0298eb
--- a/src/Tools/induct.ML	Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Tools/induct.ML	Wed Dec 31 19:54:03 2008 +0100
@@ -440,7 +440,7 @@
     val thy = ProofContext.theory_of ctxt;
     val maxidx = Thm.maxidx_of st;
     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
-    val params = rev (rename_wrt_term goal (Logic.strip_params goal));
+    val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^