# 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 *)