renamed LocalTheory.assert to affirm;
authorwenzelm
Fri Dec 15 00:08:15 2006 +0100 (2006-12-15 ago)
changeset 21860c4492c6bf450
parent 21859 03e1e75ad2e5
child 21861 a972053ed147
renamed LocalTheory.assert to affirm;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Dec 15 00:08:14 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Dec 15 00:08:15 2006 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val theory: (theory -> theory) -> local_theory -> local_theory
     1.5    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
     1.6    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.7 -  val assert: local_theory -> local_theory
     1.8 +  val affirm: local_theory -> local_theory
     1.9    val pretty: local_theory -> Pretty.T list
    1.10    val consts: (string * typ -> bool) ->
    1.11      ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
    1.12 @@ -103,7 +103,7 @@
    1.13    in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end;
    1.14  
    1.15  val target_of = #target o get_lthy;
    1.16 -val assert = tap target_of;
    1.17 +val affirm = tap target_of;
    1.18  
    1.19  fun map_target f = map_lthy (fn (theory_prefix, operations, target) =>
    1.20    (theory_prefix, operations, f target));
     2.1 --- a/src/Pure/Isar/specification.ML	Fri Dec 15 00:08:14 2006 +0100
     2.2 +++ b/src/Pure/Isar/specification.ML	Fri Dec 15 00:08:15 2006 +0100
     2.3 @@ -247,7 +247,7 @@
     2.4  fun gen_theorem prep_att prep_stmt
     2.5      kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
     2.6    let
     2.7 -    val _ = LocalTheory.assert lthy0;
     2.8 +    val _ = LocalTheory.affirm lthy0;
     2.9      val thy = ProofContext.theory_of lthy0;
    2.10  
    2.11      val (loc, ctxt, lthy) =