# HG changeset patch
# User wenzelm
# Date 1272567954 -7200
# Node ID de1862c4a308d7888c38856b539062e3bf654f02
# Parent  e31f9ac000dd488614e6c4c6d38d3aab6aae9feb
more explicit treatment of context, although not fully localized;

diff -r e31f9ac000dd -r de1862c4a308 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Thu Apr 29 20:00:26 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Thu Apr 29 21:05:54 2010 +0200
@@ -6,7 +6,7 @@
 
 signature IND_CASES =
 sig
-  val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
+  val declare: string -> (Proof.context -> conv) -> theory -> theory
   val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
   val setup: theory -> theory
 end;
@@ -19,7 +19,7 @@
 
 structure IndCasesData = Theory_Data
 (
-  type T = (simpset -> cterm -> thm) Symtab.table;
+  type T = (Proof.context -> cterm -> thm) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
@@ -28,16 +28,17 @@
 
 fun declare name f = IndCasesData.map (Symtab.update (name, f));
 
-fun smart_cases thy ss read_prop s =
+fun smart_cases ctxt s =
   let
+    val thy = ProofContext.theory_of ctxt;
     fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
-    val A = read_prop s handle ERROR msg => err msg;
+    val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
     val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
       (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
   in
     (case Symtab.lookup (IndCasesData.get thy) c of
       NONE => error ("Unknown inductive cases rule for set " ^ quote c)
-    | SOME f => f ss (Thm.cterm_of thy A))
+    | SOME f => f ctxt (Thm.cterm_of thy A))
   end;
 
 
@@ -45,10 +46,10 @@
 
 fun inductive_cases args thy =
   let
-    val mk_cases = smart_cases thy (global_simpset_of thy) (Syntax.read_prop_global thy);
+    val ctxt = ProofContext.init thy;
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute thy) srcs),
-        map (Thm.no_attributes o single o mk_cases) props));
+        map (Thm.no_attributes o single o smart_cases ctxt) props));
   in thy |> PureThy.note_thmss "" facts |> snd end;
 
 
@@ -57,10 +58,7 @@
 val setup =
   Method.setup @{binding "ind_cases"}
     (Scan.lift (Scan.repeat1 Args.name_source) >>
-      (fn props => fn ctxt =>
-        props
-        |> map (smart_cases (ProofContext.theory_of ctxt) (simpset_of ctxt) (Syntax.read_prop ctxt))
-        |> Method.erule 0))
+      (fn props => fn ctxt => Method.erule 0 (map (smart_cases ctxt) props)))
     "dynamic case analysis on sets";
 
 
diff -r e31f9ac000dd -r de1862c4a308 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Apr 29 20:00:26 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Apr 29 21:05:54 2010 +0200
@@ -268,9 +268,9 @@
       the given defs.  Cannot simply use the local con_defs because
       con_defs=[] for inference systems.
     Proposition A should have the form t:Si where Si is an inductive set*)
-  fun make_cases ss A =
+  fun make_cases ctxt A =
     rule_by_tactic
-      (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
+      (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
       (Thm.assume A RS elim)
       |> Drule.export_without_context_open;