# HG changeset patch # User wenzelm # Date 1129751570 -7200 # Node ID dfc9d3e542134d2913c83d02c49a8f22f4bf73da # Parent 308b19d78764f64fd9d81d199e2bcb2f166fe1ce removed add_inductive_x; diff -r 308b19d78764 -r dfc9d3e54213 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Wed Oct 19 21:52:49 2005 +0200 +++ b/src/ZF/Tools/inductive_package.ML Wed Oct 19 21:52:50 2005 +0200 @@ -31,8 +31,6 @@ val add_inductive_i: bool -> term list * term -> ((bstring * term) * theory attribute list) list -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result - val add_inductive_x: string list * string -> ((bstring * string) * theory attribute list) list - -> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result val add_inductive: string list * string -> ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list * (thmref * Attrib.src list) list * @@ -563,35 +561,27 @@ mutual_induct = mutual_induct}) end; - -(*external version, accepting strings*) -fun add_inductive_x (srec_tms, sdom_sum) sintrs (monos, con_defs, type_intrs, type_elims) thy = - let - val read = Sign.simple_read_term (Theory.sign_of thy); - val rec_tms = map (read Ind_Syntax.iT) srec_tms; - val dom_sum = read Ind_Syntax.iT sdom_sum; - val intr_tms = map (read propT o snd o fst) sintrs; - val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs; - in - add_inductive_i true (rec_tms, dom_sum) intr_specs - (monos, con_defs, type_intrs, type_elims) thy - end - - (*source version*) fun add_inductive (srec_tms, sdom_sum) intr_srcs (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy = let val intr_atts = map (map (Attrib.global_attribute thy) o snd) intr_srcs; + val sintrs = map fst intr_srcs ~~ intr_atts; + val read = Sign.simple_read_term thy; + val rec_tms = map (read Ind_Syntax.iT) srec_tms; + val dom_sum = read Ind_Syntax.iT sdom_sum; + val intr_tms = map (read propT o snd o fst) sintrs; + val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs; + val (thy', (((monos, con_defs), type_intrs), type_elims)) = thy |> IsarThy.apply_theorems raw_monos |>>> IsarThy.apply_theorems raw_con_defs |>>> IsarThy.apply_theorems raw_type_intrs |>>> IsarThy.apply_theorems raw_type_elims; in - add_inductive_x (srec_tms, sdom_sum) (map fst intr_srcs ~~ intr_atts) + add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims) thy' - end; + end (* outer syntax *)