# HG changeset patch
# User wenzelm
# Date 1163539015 -3600
# Node ID 4ee8e2702241c2b84f1b1660869d31d61ff85542
# Parent  3baf57a27269c7332f758a8bfcf93f6d6f836c22
InductivePackage.add_inductive_i: canonical argument order;

diff -r 3baf57a27269 -r 4ee8e2702241 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Nov 14 22:16:54 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Nov 14 22:16:55 2006 +0100
@@ -150,7 +150,7 @@
 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   let
     (* this theory is used just for parsing *)
-  
+
     val tmp_thy = thy |>
       Theory.copy |>
       Theory.add_types (map (fn (tvs, tname, mx, _) =>
@@ -186,7 +186,7 @@
       (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
     val rps = map Library.swap ps;
 
-    fun replace_types (Type ("Nominal.ABS", [T, U])) = 
+    fun replace_types (Type ("Nominal.ABS", [T, U])) =
           Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
       | replace_types (Type (s, Ts)) =
           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
@@ -221,7 +221,7 @@
 
     val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>
       let val T = nth_dtyp i
-      in map (fn (cname, dts) => 
+      in map (fn (cname, dts) =>
         let
           val Ts = map (typ_of_dtyp descr sorts') dts;
           val names = DatatypeProp.make_tnames Ts;
@@ -239,7 +239,7 @@
                         Bound i) ((length Us - 1 downto 0) ~~ Us)))
                 end
               else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
-            end;  
+            end;
         in
           (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
             (Const (List.nth (perm_names_types, i)) $
@@ -445,7 +445,7 @@
           perm_append_thms), [Simplifier.simp_add]),
          ((space_implode "_" new_type_names ^ "_perm_eq",
           perm_eq_thms), [Simplifier.simp_add])];
-  
+
     (**** Define representing sets ****)
 
     val _ = warning "representing sets";
@@ -473,7 +473,7 @@
 
     fun make_intr s T (cname, cargs) =
       let
-        fun mk_prem (dt, (j, j', prems, ts)) = 
+        fun mk_prem (dt, (j, j', prems, ts)) =
           let
             val (dts, dt') = strip_option dt;
             val (dts', dt'') = strip_dtyp dt';
@@ -513,14 +513,14 @@
                 (descr ~~ rep_set_names))));
     val rep_set_names'' = map (Sign.full_name thy3) rep_set_names';
 
-    val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
+    val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       setmp InductivePackage.quiet_mode false
         (TheoryTarget.init NONE #>
          InductivePackage.add_inductive_i false big_rep_name false true false
            (map (fn (s, T) => (s, SOME (T --> HOLogic.boolT), NoSyn))
               (rep_set_names' ~~ recTs'))
            [] (map (fn x => (("", []), x)) intr_ts) [] #>
-         apfst (ProofContext.theory_of o LocalTheory.exit)) thy3;
+         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy3;
 
     (**** Prove that representing set is closed under permutation ****)
 
@@ -547,7 +547,7 @@
            [indtac rep_induct [] 1,
             ALLGOALS (simp_tac (simpset_of thy4 addsimps
               (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
-            ALLGOALS (resolve_tac rep_intrs 
+            ALLGOALS (resolve_tac rep_intrs
                THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
         length new_type_names));
 
@@ -669,8 +669,8 @@
     fun strip_suffix i s = implode (List.take (explode s, size s - i));
 
     (** strips the "_Rep" in type names *)
-    fun strip_nth_name i s = 
-      let val xs = NameSpace.unpack s; 
+    fun strip_nth_name i s =
+      let val xs = NameSpace.unpack s;
       in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val (descr'', ndescr) = ListPair.unzip (List.mapPartial
@@ -767,7 +767,7 @@
     val rep_inject_thms = map (#Rep_inject o fst) typedefs
 
     (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
-    
+
     fun prove_constr_rep_thm eqn =
       let
         val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
@@ -829,7 +829,7 @@
     val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
       let val T = nth_dtyp' i
       in List.concat (map (fn (atom, perm_closed_thms) =>
-          map (fn ((cname, dts), constr_rep_thm) => 
+          map (fn ((cname, dts), constr_rep_thm) =>
         let
           val cname = Sign.intern_const thy8
             (NameSpace.append tname (Sign.base_name cname));
@@ -1343,7 +1343,7 @@
 
     val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts' used;
 
-    val rec_sort = if null dt_atomTs then HOLogic.typeS else 
+    val rec_sort = if null dt_atomTs then HOLogic.typeS else
       let val names = map (Sign.base_name o fst o dest_Type) dt_atomTs
       in Sign.certify_sort thy10 (map (Sign.intern_class thy10)
         (map (fn s => "pt_" ^ s) names @
@@ -1440,7 +1440,7 @@
         Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
           (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets');
 
-    val (thy11, {intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}) =
+    val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10 |>
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (TheoryTarget.init NONE #>
@@ -1448,7 +1448,7 @@
            (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map (apsnd SOME o dest_Free) rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) [] #>
-         apfst (ProofContext.theory_of o LocalTheory.exit)) |>>
+         apsnd (ProofContext.theory_of o LocalTheory.exit)) ||>
       PureThy.hide_thms true [NameSpace.append
         (Sign.full_name thy10 big_rec_name) "induct"];
 
@@ -1875,7 +1875,7 @@
                               THEN resolve_tac rec_prems 1),
                             resolve_tac P_ind_ths 1,
                             REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
-        
+
                     val fresh_results'' = map prove_fresh_result boundsl;
 
                     fun prove_fresh_result'' ((a as Free (_, aT), b), th) =
@@ -1989,7 +1989,7 @@
              REPEAT (solve (prems @ rec_total_thms) prems 1)])
       end) (rec_eq_prems ~~
         DatatypeProp.make_primrecs new_type_names descr' sorts' thy12);
-    
+
     (* FIXME: theorems are stored in database for testing only *)
     val (_, thy13) = thy12 |>
       PureThy.add_thmss
@@ -2032,4 +2032,3 @@
 end;
 
 end
-
diff -r 3baf57a27269 -r 4ee8e2702241 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Nov 14 22:16:54 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Nov 14 22:16:55 2006 +0100
@@ -157,14 +157,14 @@
       Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
         (([], 0), descr' ~~ recTs ~~ rec_sets');
 
-    val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
+    val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (TheoryTarget.init NONE #>
          InductivePackage.add_inductive_i false big_rec_name' false false true
            (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map (apsnd SOME o dest_Free) rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) [] #>
-         apfst (ProofContext.theory_of o LocalTheory.exit)) thy0;
+         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
diff -r 3baf57a27269 -r 4ee8e2702241 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Nov 14 22:16:54 2006 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Nov 14 22:16:55 2006 +0100
@@ -173,13 +173,13 @@
       map (make_intr rep_set_name (length constrs))
         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'));
 
-    val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
+    val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (TheoryTarget.init NONE #>
          InductivePackage.add_inductive_i false big_rec_name false true false
            (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) [] #>
-         apfst (ProofContext.theory_of o LocalTheory.exit)) thy1;
+         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy1;
 
     (********************************* typedef ********************************)
 
diff -r 3baf57a27269 -r 4ee8e2702241 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 14 22:16:54 2006 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 14 22:16:55 2006 +0100
@@ -40,7 +40,7 @@
     let
       val qdefs = map dest_all_all defs
                   
-      val (lthy, {intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}) =
+      val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}, lthy) =
           InductivePackage.add_inductive_i true (*verbose*)
                                            "" (* no altname *)
                                            false (* no coind *)
@@ -74,4 +74,3 @@
     end
     
 end
-