# HG changeset patch
# User huffman
# Date 1272755604 25200
# Node ID 4c1f119fadb94165a49a1b059a9fe9532c53f493
# Parent  aa1f8acdcc1c7f5e8dc7d2b50069033398e8edc9# Parent  5479681ab465f5d6bcb8fbb22092cdb44bf44616
merged

diff -r aa1f8acdcc1c -r 4c1f119fadb9 Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats	Sat May 01 11:46:47 2010 -0700
+++ b/Admin/isatest/isatest-stats	Sat May 01 16:13:24 2010 -0700
@@ -6,7 +6,7 @@
 
 THIS=$(cd "$(dirname "$0")"; pwd -P)
 
-PLATFORMS="at-poly at-poly-test at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
+PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
 
 ISABELLE_SESSIONS="\
   HOL-Plain \
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/FOL/simpdata.ML	Sat May 01 16:13:24 2010 -0700
@@ -35,10 +35,6 @@
   [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
    ("All", [@{thm spec}]), ("True", []), ("False", [])];
 
-(* ###FIXME: move to simplifier.ML
-val mk_atomize:      (string * thm list) list -> thm -> thm list
-*)
-(* ###FIXME: move to simplifier.ML *)
 fun mk_atomize pairs =
   let fun atoms th =
         (case concl_of th of
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/FOLP/simp.ML	Sat May 01 16:13:24 2010 -0700
@@ -222,7 +222,7 @@
 fun normed_rews congs =
   let val add_norms = add_norm_tags congs in
     fn thm => Variable.tradeT
-      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm]
+      (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm]
   end;
 
 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Library/Efficient_Nat.thy	Sat May 01 16:13:24 2010 -0700
@@ -152,7 +152,8 @@
       in
         case map_filter (fn th'' =>
             SOME (th'', singleton
-              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
+              (Variable.trade (K (fn [th'''] => [th''' RS th']))
+                (Variable.global_thm_context th'')) th'')
           handle THM _ => NONE) thms of
             [] => NONE
           | thps =>
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sat May 01 16:13:24 2010 -0700
@@ -342,8 +342,8 @@
         ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
           [Classical.safe_elim NONE]),
         ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
-        ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
-        @ named_rules @ unnamed_rules)
+        ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+          named_rules @ unnamed_rules)
     |> snd
     |> add_case_tr' case_names
     |> register dt_infos
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat May 01 16:13:24 2010 -0700
@@ -355,7 +355,7 @@
   if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
   else
     let
-      val ctxt0 = Variable.thm_context th
+      val ctxt0 = Variable.global_thm_context th
       val (nnfth, ctxt1) = to_nnf th ctxt0
       val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
     in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
@@ -408,7 +408,7 @@
 local
 
 fun skolem_def (name, th) thy =
-  let val ctxt0 = Variable.thm_context th in
+  let val ctxt0 = Variable.global_thm_context th in
     (case try (to_nnf th) ctxt0 of
       NONE => (NONE, thy)
     | SOME (nnfth, ctxt1) =>
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/meson.ML	Sat May 01 16:13:24 2010 -0700
@@ -555,7 +555,7 @@
         skolemize_nnf_list ctxt ths);
 
 fun add_clauses th cls =
-  let val ctxt0 = Variable.thm_context th
+  let val ctxt0 = Variable.global_thm_context th
       val (cnfs, ctxt) = make_cnf [] th ctxt0
   in Variable.export ctxt ctxt0 cnfs @ cls end;
 
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/simpdata.ML	Sat May 01 16:13:24 2010 -0700
@@ -95,7 +95,7 @@
         fun res th = map (fn rl => th RS rl);   (*exception THM*)
         fun res_fixed rls =
           if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
-          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm];
+          else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
       in
         case concl_of thm
           of Const (@{const_name Trueprop}, _) $ p => (case head_of p
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/Provers/clasimp.ML	Sat May 01 16:13:24 2010 -0700
@@ -70,8 +70,14 @@
 fun get_css context = (Classical.get_cs context, Simplifier.get_ss context);
 
 fun map_css f context =
-  let val (cs', ss') = f (get_css context)
-  in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
+  let
+    val (cs, ss) = get_css context;
+    val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss);
+  in
+    context
+    |> Classical.map_cs (K cs')
+    |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss'))
+  end;
 
 fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
 
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/Pure/simplifier.ML	Sat May 01 16:13:24 2010 -0700
@@ -37,6 +37,7 @@
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
   val global_context: theory  -> simpset -> simpset
+  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/Pure/variable.ML	Sat May 01 16:13:24 2010 -0700
@@ -28,7 +28,7 @@
   val declare_typ: typ -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
   val declare_thm: thm -> Proof.context -> Proof.context
-  val thm_context: thm -> Proof.context
+  val global_thm_context: thm -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
   val bind_term: indexname * term option -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
@@ -235,7 +235,7 @@
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
-fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
+fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
 
 
 (* renaming term/type frees *)
diff -r aa1f8acdcc1c -r 4c1f119fadb9 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat May 01 11:46:47 2010 -0700
+++ b/src/Tools/induct.ML	Sat May 01 16:13:24 2010 -0700
@@ -46,7 +46,8 @@
   val coinduct_pred: string -> attribute
   val coinduct_del: attribute
   val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
-  val add_simp_rule: attribute
+  val induct_simp_add: attribute
+  val induct_simp_del: attribute
   val no_simpN: string
   val casesN: string
   val inductN: string
@@ -320,8 +321,14 @@
 val coinduct_del = del_att map3;
 
 fun map_simpset f = InductData.map (map4 f);
-fun add_simp_rule (ctxt, thm) =
-  (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm);
+
+fun induct_simp f =
+  Thm.declaration_attribute (fn thm => fn context =>
+      (map_simpset
+        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
+
+val induct_simp_add = induct_simp (op addsimps);
+val induct_simp_del = induct_simp (op delsimps);
 
 end;
 
@@ -359,7 +366,7 @@
     "declaration of induction rule" #>
   Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
     "declaration of coinduction rule" #>
-  Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule)
+  Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
     "declaration of rules for simplifying induction or cases rules";
 
 end;