# HG changeset patch # User wenzelm # Date 1008327038 -3600 # Node ID 58848edad3c4e40f3f9e9e9e6f75596fa3fe6945 # Parent de2575b6cd380eb7b09375c55e952bfecf2bdbb1 changed Type.varify; diff -r de2575b6cd38 -r 58848edad3c4 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Fri Dec 14 11:50:19 2001 +0100 +++ b/src/HOL/Tools/inductive_package.ML Fri Dec 14 11:50:38 2001 +0100 @@ -182,7 +182,7 @@ val add_term_consts_2 = foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs); fun varify (t, (i, ts)) = - let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) + let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, []))) in (maxidx_of_term t', t'::ts) end; val (i, cs') = foldr varify (cs, (~1, [])); val (i', intr_ts') = foldr varify (intr_ts, (i, []));