# HG changeset patch
# User haftmann
# Date 1213104664 -7200
# Node ID 661a74bafeb797ff7ac580e75431d5ffe4ede798
# Parent  c19be97e4553fdd29144fb5ee52d2265c328f523
polished interface of datatype package

diff -r c19be97e4553 -r 661a74bafeb7 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 15:31:03 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 10 15:31:04 2008 +0200
@@ -65,7 +65,7 @@
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
           let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
-              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype_i true false [ak] [dt] thy
+              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
               val inject_flat = Library.flat inject
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
diff -r c19be97e4553 -r 661a74bafeb7 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Jun 10 15:31:03 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Jun 10 15:31:04 2008 +0200
@@ -248,7 +248,7 @@
     val full_new_type_names' = map (Sign.full_name thy) new_type_names';
 
     val ({induction, ...},thy1) =
-      DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
+      DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
 
     val SOME {descr, ...} = Symtab.lookup
       (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
diff -r c19be97e4553 -r 661a74bafeb7 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 10 15:31:03 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 10 15:31:04 2008 +0200
@@ -312,7 +312,7 @@
     val ((dummies, dt_info), thy2) =
       thy1
       |> add_dummies
-           (DatatypePackage.add_datatype_i false false (map #2 dts))
+           (DatatypePackage.add_datatype false false (map #2 dts))
            (map (pair false) dts) []
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;
diff -r c19be97e4553 -r 661a74bafeb7 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jun 10 15:31:03 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jun 10 15:31:04 2008 +0200
@@ -647,7 +647,7 @@
       fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
       val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
       val tacs = [
-        DatatypePackage.induct_tac "n" 1,
+        DatatypePackage.induct_tac @{context} "n" 1,
         simp_tac iterate_Cprod_ss 1,
         asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
     in pg copy_take_defs goal tacs end;
@@ -678,7 +678,7 @@
       fun eq_tacs ((dn, _), cons) = map con_tac cons;
       val tacs =
         simp_tac iterate_Cprod_ss 1 ::
-        DatatypePackage.induct_tac "n" 1 ::
+        DatatypePackage.induct_tac @{context} "n" 1 ::
         simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
         TRY (safe_tac HOL_cs) ::
@@ -750,7 +750,7 @@
           val tacs1 = [
             quant_tac 1,
             simp_tac HOL_ss 1,
-            DatatypePackage.induct_tac "n" 1,
+            DatatypePackage.induct_tac @{context} "n" 1,
             simp_tac (take_ss addsimps prems) 1,
             TRY (safe_tac HOL_cs)];
           fun arg_tac arg =
@@ -845,7 +845,7 @@
               maps con_tacs cons;
             val tacs =
               rtac allI 1 ::
-              DatatypePackage.induct_tac "n" 1 ::
+              DatatypePackage.induct_tac @{context}  "n" 1 ::
               simp_tac take_ss 1 ::
               TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
               flat (mapn foo_tacs 1 (conss ~~ cases));
@@ -938,7 +938,7 @@
         REPEAT (CHANGED (asm_simp_tac take_ss 1))];
       val tacs = [
         rtac impI 1,
-        DatatypePackage.induct_tac "n" 1,
+        DatatypePackage.induct_tac @{context} "n" 1,
         simp_tac take_ss 1,
         safe_tac HOL_cs] @
         flat (mapn x_tacs 0 xs);