# HG changeset patch
# User wenzelm
# Date 1190660861 -7200
# Node ID b5e68fe31eba8552adf8887e57d6bfc3815f860c
# Parent  2892482a4e6296b43cadc57f6d6a33e007ad1f5d
added @{theory_ref};

diff -r 2892482a4e62 -r b5e68fe31eba src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Sep 24 21:07:40 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Sep 24 21:07:41 2007 +0200
@@ -207,6 +207,12 @@
     >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
   || Scan.succeed ("thy", "ML_Context.the_context ()"));
 
+val _ = ML_Context.value_antiq "theory_ref"
+  (Scan.lift Args.name
+    >> (fn name => (name ^ "_thy",
+        "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")"))
+  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_context ())"));
+
 
 
 (** thy operations **)