# HG changeset patch
# User wenzelm
# Date 1257461963 -3600
# Node ID a4a38ed813f766ce0042ec6a597ed478ba54b27e
# Parent  ae1f5d89b082de682b15f71690aa03dc3798a031
tuned;

diff -r ae1f5d89b082 -r a4a38ed813f7 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 05 22:59:57 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 05 23:59:23 2009 +0100
@@ -338,8 +338,7 @@
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
   in
     thy2
-    |> Context.the_theory o fold (fold Nitpick_Simps.add_thm) case_thms
-       o Context.Theory
+    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
     |> Sign.parent_path
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
diff -r ae1f5d89b082 -r a4a38ed813f7 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Nov 05 22:59:57 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Nov 05 23:59:23 2009 +0100
@@ -778,12 +778,14 @@
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
       params intr_ts rec_preds_defs lthy1;
-    val elims = if no_elim then [] else
-      prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
-        unfold rec_preds_defs lthy1;
+    val elims =
+      if no_elim then []
+      else
+        prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
+          unfold rec_preds_defs lthy1;
     val raw_induct = zero_var_indexes
-      (if no_ind then Drule.asm_rl else
-       if coind then
+      (if no_ind then Drule.asm_rl
+       else if coind then
          singleton (ProofContext.export
            (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
            (rotate_prems ~1 (ObjectLogic.rulify
diff -r ae1f5d89b082 -r a4a38ed813f7 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Nov 05 22:59:57 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 05 23:59:23 2009 +0100
@@ -520,10 +520,10 @@
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     val (intrs', elims', induct, lthy4) =
       Inductive.declare_rules kind rec_name coind no_ind cnames
-      (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
-      (map (fn th => (to_set [] (Context.Proof lthy3) th,
-         map fst (fst (Rule_Cases.get th)))) elims)
-      raw_induct' lthy3
+        (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
+        (map (fn th => (to_set [] (Context.Proof lthy3) th,
+           map fst (fst (Rule_Cases.get th)))) elims)
+        raw_induct' lthy3;
   in
     ({intrs = intrs', elims = elims', induct = induct,
       raw_induct = raw_induct', preds = map fst defs},