--- a/src/Pure/Isar/local_theory.ML Sat Oct 14 23:25:51 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML Sat Oct 14 23:25:53 2006 +0200
@@ -17,6 +17,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 pretty: local_theory -> Pretty.T list
val consts: (string * typ -> bool) ->
((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
@@ -90,6 +91,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;
fun map_target f = map_lthy (fn (theory_prefix, operations, target) =>
(theory_prefix, operations, f target));