# HG changeset patch
# User wenzelm
# Date 1166137695 -3600
# Node ID c4492c6bf4504f3fe56197d09e696951ebb384f4
# Parent  03e1e75ad2e51f8354874a40c6bc98d9b78b36c3
renamed LocalTheory.assert to affirm;

diff -r 03e1e75ad2e5 -r c4492c6bf450 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Dec 15 00:08:14 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Dec 15 00:08:15 2006 +0100
@@ -18,7 +18,7 @@
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
-  val assert: local_theory -> local_theory
+  val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val consts: (string * typ -> bool) ->
     ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
@@ -103,7 +103,7 @@
   in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end;
 
 val target_of = #target o get_lthy;
-val assert = tap target_of;
+val affirm = tap target_of;
 
 fun map_target f = map_lthy (fn (theory_prefix, operations, target) =>
   (theory_prefix, operations, f target));
diff -r 03e1e75ad2e5 -r c4492c6bf450 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Dec 15 00:08:14 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Dec 15 00:08:15 2006 +0100
@@ -247,7 +247,7 @@
 fun gen_theorem prep_att prep_stmt
     kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 =
   let
-    val _ = LocalTheory.assert lthy0;
+    val _ = LocalTheory.affirm lthy0;
     val thy = ProofContext.theory_of lthy0;
 
     val (loc, ctxt, lthy) =