# HG changeset patch # User wenzelm # Date 1160861153 -7200 # Node ID 99697a1597b2d67a0fe3fbb2e60023d457edf38d # Parent 82f44ceb4fa3e2c64c60908e63d273ebbe5f5234 added assert; diff -r 82f44ceb4fa3 -r 99697a1597b2 src/Pure/Isar/local_theory.ML --- 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));