--- a/src/HOL/Tools/inductive_package.ML Tue Jul 19 17:21:46 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Tue Jul 19 17:21:47 2005 +0200
@@ -180,7 +180,7 @@
val tsig = Sign.tsig_of thy;
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
- let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
+ let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
in (maxidx_of_term t', t'::ts) end;
val (i, cs') = foldr varify (~1, []) cs;
val (i', intr_ts') = foldr varify (i, []) intr_ts;