# HG changeset patch
# User wenzelm
# Date 1169298562 -3600
# Node ID 8134eb5f45015e3bcc5980b54ccfa3d92973eee3
# Parent  faff42afeacdfb86c37c58e723ed6368f324a765
added @{theory};

diff -r faff42afeacd -r 8134eb5f4501 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Jan 20 14:09:21 2007 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Jan 20 14:09:22 2007 +0100
@@ -202,6 +202,11 @@
 
 fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));
 
+val _ = ML_Context.value_antiq "theory"
+  (Scan.lift Args.name
+    >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
+  || Scan.succeed ("thy", "ML_Context.the_context_finished ()"));
+
 
 
 (** thy operations **)