src/HOL/Tools/inductive_package.ML
changeset 12494 58848edad3c4
parent 12400 f12f95e216e0
child 12527 d6c91bc3e49c
equal deleted inserted replaced
12493:de2575b6cd38 12494:58848edad3c4
   180   (let
   180   (let
   181     val {tsig, ...} = Sign.rep_sg sign;
   181     val {tsig, ...} = Sign.rep_sg sign;
   182     val add_term_consts_2 =
   182     val add_term_consts_2 =
   183       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   183       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   184     fun varify (t, (i, ts)) =
   184     fun varify (t, (i, ts)) =
   185       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   185       let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
   186       in (maxidx_of_term t', t'::ts) end;
   186       in (maxidx_of_term t', t'::ts) end;
   187     val (i, cs') = foldr varify (cs, (~1, []));
   187     val (i, cs') = foldr varify (cs, (~1, []));
   188     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   188     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   189     val rec_consts = foldl add_term_consts_2 ([], cs');
   189     val rec_consts = foldl add_term_consts_2 ([], cs');
   190     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   190     val intr_consts = foldl add_term_consts_2 ([], intr_ts');