renamed functor ProjectRuleFun to Project_Rule;
authorwenzelm
Fri Jul 24 18:58:58 2009 +0200 (2009-07-24)
changeset 32172c4e55f30d527
parent 32171 220abde9962b
child 32173 34f7b0fbe047
renamed functor ProjectRuleFun to Project_Rule;
renamed structure ProjectRule to Project_Rule;
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/inductive.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Tools/project_rule.ML
     1.1 --- a/src/FOL/IFOL.thy	Fri Jul 24 12:33:00 2009 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Fri Jul 24 18:58:58 2009 +0200
     1.3 @@ -591,12 +591,12 @@
     1.4    done
     1.5  
     1.6  ML {*
     1.7 -structure ProjectRule = ProjectRuleFun
     1.8 -(struct
     1.9 +structure Project_Rule = Project_Rule
    1.10 +(
    1.11    val conjunct1 = @{thm conjunct1}
    1.12    val conjunct2 = @{thm conjunct2}
    1.13    val mp = @{thm mp}
    1.14 -end)
    1.15 +)
    1.16  *}
    1.17  
    1.18  use "fologic.ML"
     2.1 --- a/src/HOL/HOL.thy	Fri Jul 24 12:33:00 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Jul 24 18:58:58 2009 +0200
     2.3 @@ -1390,7 +1390,7 @@
     2.4  text {* Rule projections: *}
     2.5  
     2.6  ML {*
     2.7 -structure ProjectRule = ProjectRuleFun
     2.8 +structure Project_Rule = Project_Rule
     2.9  (
    2.10    val conjunct1 = @{thm conjunct1}
    2.11    val conjunct2 = @{thm conjunct2}
     3.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Jul 24 12:33:00 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Jul 24 18:58:58 2009 +0200
     3.3 @@ -152,7 +152,7 @@
     3.4  val meta_spec = thm "meta_spec";
     3.5  
     3.6  fun projections rule =
     3.7 -  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     3.8 +  Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     3.9    |> map (standard #> RuleCases.save rule);
    3.10  
    3.11  val supp_prod = thm "supp_prod";
     4.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 24 12:33:00 2009 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 24 18:58:58 2009 +0200
     4.3 @@ -566,7 +566,7 @@
     4.4              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
     4.5            ctxt;
     4.6          val strong_inducts =
     4.7 -          ProjectRule.projects ctxt (1 upto length names) strong_induct'
     4.8 +          Project_Rule.projects ctxt (1 upto length names) strong_induct'
     4.9        in
    4.10          ctxt' |>
    4.11          LocalTheory.note Thm.generatedK
     5.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 24 12:33:00 2009 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 24 18:58:58 2009 +0200
     5.3 @@ -466,7 +466,7 @@
     5.4              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
     5.5            ctxt;
     5.6          val strong_inducts =
     5.7 -          ProjectRule.projects ctxt' (1 upto length names) strong_induct'
     5.8 +          Project_Rule.projects ctxt' (1 upto length names) strong_induct'
     5.9        in
    5.10          ctxt' |>
    5.11          LocalTheory.note Thm.generatedK
     6.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Jul 24 12:33:00 2009 +0200
     6.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Jul 24 18:58:58 2009 +0200
     6.3 @@ -191,7 +191,7 @@
     6.4  
     6.5  fun add_cases_induct infos induction thy =
     6.6    let
     6.7 -    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
     6.8 +    val inducts = Project_Rule.projections (ProofContext.init thy) induction;
     6.9  
    6.10      fun named_rules (name, {index, exhaustion, ...}: info) =
    6.11        [((Binding.empty, nth inducts index), [Induct.induct_type name]),
     7.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 24 12:33:00 2009 +0200
     7.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 24 18:58:58 2009 +0200
     7.3 @@ -712,7 +712,7 @@
     7.4            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
     7.5  
     7.6      val ctxt3 = if no_ind orelse coind then ctxt2 else
     7.7 -      let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
     7.8 +      let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
     7.9        in
    7.10          ctxt2 |>
    7.11          LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
     8.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Jul 24 12:33:00 2009 +0200
     8.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Jul 24 18:58:58 2009 +0200
     8.3 @@ -1033,7 +1033,7 @@
     8.4      in pg [] goal (K tacs) end;
     8.5  end; (* local *)
     8.6  
     8.7 -val inducts = ProjectRule.projections (ProofContext.init thy) ind;
     8.8 +val inducts = Project_Rule.projections (ProofContext.init thy) ind;
     8.9  fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
    8.10  val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
    8.11  
     9.1 --- a/src/Tools/project_rule.ML	Fri Jul 24 12:33:00 2009 +0200
     9.2 +++ b/src/Tools/project_rule.ML	Fri Jul 24 18:58:58 2009 +0200
     9.3 @@ -24,7 +24,7 @@
     9.4    val projections: Proof.context -> thm -> thm list
     9.5  end;
     9.6  
     9.7 -functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
     9.8 +functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE =
     9.9  struct
    9.10  
    9.11  fun conj1 th = th RS Data.conjunct1;