# HG changeset patch
# User wenzelm
# Date 1150234894 -7200
# Node ID cc4b2b882e4cdb897eb23413e3dd2580422eabb3
# Parent  588329441a7885f32eede668d70e67dafa2377b9
ProjectRule now context dependent;

diff -r 588329441a78 -r cc4b2b882e4c src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:31 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:34 2006 +0200
@@ -133,7 +133,7 @@
 val meta_spec = thm "meta_spec";
 
 fun projections rule =
-  ProjectRule.projections rule
+  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
   |> map (standard #> RuleCases.save rule);
 
 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
diff -r 588329441a78 -r cc4b2b882e4c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jun 13 23:41:31 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 13 23:41:34 2006 +0200
@@ -316,22 +316,20 @@
 
 (* add_cases_induct *)
 
-fun add_cases_induct infos induction =
+fun add_cases_induct infos induction thy =
   let
-    val n = length (HOLogic.dest_concls (Thm.concl_of induction));
-    fun proj i = ProjectRule.project induction (i + 1);
+    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
 
     fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
-      [(("", proj index), [InductAttrib.induct_type name]),
+      [(("", nth inducts index), [InductAttrib.induct_type name]),
        (("", exhaustion), [InductAttrib.cases_type name])];
     fun unnamed_rule i =
-      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
+      (("", nth inducts i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
   in
-    PureThy.add_thms
+    thy |> PureThy.add_thms
       (List.concat (map named_rules infos) @
-        map unnamed_rule (length infos upto n - 1)) #> snd #>
-    PureThy.add_thmss [(("inducts",
-      map (proj #> standard #> RuleCases.save induction) (0 upto n - 1)), [])] #> snd
+        map unnamed_rule (length infos upto length inducts - 1)) |> snd
+    |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
   end;
 
 
@@ -801,7 +799,7 @@
       ||>> apply_theorems [raw_induction];
     val sign = Theory.sign_of thy1;
 
-    val induction' = freezeT induction;
+    val induction' = Thm.freezeT induction;
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Sign.string_of_term sign t);
diff -r 588329441a78 -r cc4b2b882e4c src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Jun 13 23:41:31 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Jun 13 23:41:34 2006 +0200
@@ -436,17 +436,19 @@
     val cases_specs = if no_elim then [] else map2 cases_spec names elims;
 
     val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
-    val induct_specs =
-      if no_induct then I
+    fun induct_specs thy =
+      if no_induct then thy
       else
         let
-          val rules = names ~~ map (ProjectRule.project induct) (1 upto length names);
+          val ctxt = ProofContext.init thy;
+          val rules = names ~~ ProjectRule.projects ctxt (1 upto length names) induct;
           val inducts = map (RuleCases.save induct o standard o #2) rules;
         in
-          PureThy.add_thms (rules |> map (fn (name, th) =>
-            (("", th), [RuleCases.consumes 1, induct_att name]))) #> snd #>
-          PureThy.add_thmss
-            [((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] #> snd
+          thy
+          |> PureThy.add_thms (rules |> map (fn (name, th) =>
+            (("", th), [RuleCases.consumes 1, induct_att name]))) |> snd
+          |> PureThy.add_thmss
+            [((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] |> snd
         end;
   in Library.apply cases_specs #> induct_specs end;
 
diff -r 588329441a78 -r cc4b2b882e4c src/Provers/project_rule.ML
--- a/src/Provers/project_rule.ML	Tue Jun 13 23:41:31 2006 +0200
+++ b/src/Provers/project_rule.ML	Tue Jun 13 23:41:34 2006 +0200
@@ -17,8 +17,9 @@
 
 signature PROJECT_RULE =
 sig
-  val project: thm -> int -> thm
-  val projections: thm -> thm list
+  val project: Proof.context -> int -> thm -> thm
+  val projects: Proof.context -> int list -> thm -> thm list
+  val projections: Proof.context -> thm -> thm list
 end;
 
 functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
@@ -28,9 +29,7 @@
 fun conj2 th = th RS Data.conjunct2;
 fun imp th = th RS Data.mp;
 
-val freeze = Drule.zero_var_indexes #> Drule.freeze_all;
-
-fun project rule i =
+fun projects ctxt is raw_rule =
   let
     fun proj 1 th = the_default th (try conj1 th)
       | proj k th = proj (k - 1) (conj2 th);
@@ -38,24 +37,27 @@
       (case try imp th of
         NONE => (k, th)
       | SOME th' => prems (k + 1) th');
-  in
-    rule
-    |> freeze
-    |> proj i
-    |> prems 0 |-> (fn k =>
-      Thm.permute_prems 0 (~ k)
-      #> Drule.standard'
-      #> RuleCases.save rule
-      #> RuleCases.add_consumes k)
-  end;
+    val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
+    fun result i =
+      rule
+      |> proj i
+      |> prems 0 |-> (fn k =>
+        Thm.permute_prems 0 (~ k)
+        #> ProofContext.export ctxt' ctxt
+        #> Drule.zero_var_indexes
+        #> RuleCases.save raw_rule
+        #> RuleCases.add_consumes k);
+  in map result is end;
 
-fun projections rule =
+fun project ctxt i th = hd (projects ctxt [i] th);
+
+fun projections ctxt raw_rule =
   let
     fun projs k th =
       (case try conj2 th of
         NONE => k
       | SOME th' => projs (k + 1) th');
-    val n = projs 1 (freeze rule);
-  in map (project rule) (1 upto n) end;
+    val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
+  in projects ctxt (1 upto projs 1 rule) raw_rule end;
 
 end;