changed Type.varify;
authorwenzelm
Fri Dec 14 11:50:38 2001 +0100 (2001-12-14 ago)
changeset 1249458848edad3c4
parent 12493 de2575b6cd38
child 12495 89f97fa683f5
changed Type.varify;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Dec 14 11:50:19 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 14 11:50:38 2001 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4      val add_term_consts_2 =
     1.5        foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
     1.6      fun varify (t, (i, ts)) =
     1.7 -      let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
     1.8 +      let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     1.9        in (maxidx_of_term t', t'::ts) end;
    1.10      val (i, cs') = foldr varify (cs, (~1, []));
    1.11      val (i', intr_ts') = foldr varify (intr_ts, (i, []));