--- 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 **)