ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
recovered @{theory_ref NAME} (cf. 1f09a22a1027);
--- a/NEWS Wed Jul 21 14:27:05 2010 +0200
+++ b/NEWS Wed Jul 21 15:02:51 2010 +0200
@@ -103,6 +103,15 @@
similar to inductive_cases.
+*** ML ***
+
+* ML antiquotations @{theory} and @{theory_ref} refer to named
+theories from the ancestry of the current context, not any accidental
+theory loader state as before. Potential INCOMPATIBILITY, subtle
+change in semantics.
+
+
+
New in Isabelle2009-2 (June 2010)
---------------------------------
--- a/src/Pure/ML/ml_antiquote.ML Wed Jul 21 14:27:05 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Wed Jul 21 15:02:51 2010 +0200
@@ -64,12 +64,14 @@
>> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
- (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
+ (Scan.lift Args.name >> (fn name =>
+ "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
|| Scan.succeed "ML_Context.the_global_context ()");
val _ = value "theory_ref"
(Scan.lift Args.name >> (fn name =>
- "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
+ "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
+ ML_Syntax.print_string name ^ ")")
|| Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");