# HG changeset patch # User wenzelm # Date 1230816219 -3600 # Node ID 8fb76724582236d1bb89e27f9498a468e6baa5c7 # Parent f45c9c3b40a379216e645ad7674901b5294dca4a Term.add_consts; diff -r f45c9c3b40a3 -r 8fb767245822 src/HOL/Tools/old_primrec_package.ML --- a/src/HOL/Tools/old_primrec_package.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/HOL/Tools/old_primrec_package.ML Thu Jan 01 14:23:39 2009 +0100 @@ -34,14 +34,13 @@ same type in all introduction rules*) fun unify_consts thy cs intr_ts = (let - val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I); fun varify (t, (i, ts)) = let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (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; - val rec_consts = fold add_term_consts_2 cs' []; - val intr_consts = fold add_term_consts_2 intr_ts' []; + val rec_consts = fold Term.add_consts cs' []; + val intr_consts = fold Term.add_consts intr_ts' []; fun unify (cname, cT) = let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts) in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;