# HG changeset patch
# User wenzelm
# Date 1248454738 -7200
# Node ID c4e55f30d527150cefd6b9b45db8e2f3a7f7a60c
# Parent  220abde9962b59d833be2f461d9882f9f60f3d34
renamed functor ProjectRuleFun to Project_Rule;
renamed structure ProjectRule to Project_Rule;

diff -r 220abde9962b -r c4e55f30d527 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/FOL/IFOL.thy	Fri Jul 24 18:58:58 2009 +0200
@@ -591,12 +591,12 @@
   done
 
 ML {*
-structure ProjectRule = ProjectRuleFun
-(struct
+structure Project_Rule = Project_Rule
+(
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
   val mp = @{thm mp}
-end)
+)
 *}
 
 use "fologic.ML"
diff -r 220abde9962b -r c4e55f30d527 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 24 18:58:58 2009 +0200
@@ -1390,7 +1390,7 @@
 text {* Rule projections: *}
 
 ML {*
-structure ProjectRule = ProjectRuleFun
+structure Project_Rule = Project_Rule
 (
   val conjunct1 = @{thm conjunct1}
   val conjunct2 = @{thm conjunct2}
diff -r 220abde9962b -r c4e55f30d527 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -152,7 +152,7 @@
 val meta_spec = thm "meta_spec";
 
 fun projections rule =
-  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
+  Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
   |> map (standard #> RuleCases.save rule);
 
 val supp_prod = thm "supp_prod";
diff -r 220abde9962b -r c4e55f30d527 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -566,7 +566,7 @@
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
         val strong_inducts =
-          ProjectRule.projects ctxt (1 upto length names) strong_induct'
+          Project_Rule.projects ctxt (1 upto length names) strong_induct'
       in
         ctxt' |>
         LocalTheory.note Thm.generatedK
diff -r 220abde9962b -r c4e55f30d527 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -466,7 +466,7 @@
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
         val strong_inducts =
-          ProjectRule.projects ctxt' (1 upto length names) strong_induct'
+          Project_Rule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
         LocalTheory.note Thm.generatedK
diff -r 220abde9962b -r c4e55f30d527 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -191,7 +191,7 @@
 
 fun add_cases_induct infos induction thy =
   let
-    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
+    val inducts = Project_Rule.projections (ProofContext.init thy) induction;
 
     fun named_rules (name, {index, exhaustion, ...}: info) =
       [((Binding.empty, nth inducts index), [Induct.induct_type name]),
diff -r 220abde9962b -r c4e55f30d527 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -712,7 +712,7 @@
           map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
     val ctxt3 = if no_ind orelse coind then ctxt2 else
-      let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
+      let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
       in
         ctxt2 |>
         LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
diff -r 220abde9962b -r c4e55f30d527 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -1033,7 +1033,7 @@
     in pg [] goal (K tacs) end;
 end; (* local *)
 
-val inducts = ProjectRule.projections (ProofContext.init thy) ind;
+val inducts = Project_Rule.projections (ProofContext.init thy) ind;
 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
 val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
 
diff -r 220abde9962b -r c4e55f30d527 src/Tools/project_rule.ML
--- a/src/Tools/project_rule.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/Tools/project_rule.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -24,7 +24,7 @@
   val projections: Proof.context -> thm -> thm list
 end;
 
-functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
+functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE =
 struct
 
 fun conj1 th = th RS Data.conjunct1;