thm_antiq: produce error at runtime, not compile time;
tuned;

--- a/src/Pure/ML/ml_context.ML	Thu Mar 20 17:38:54 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 17:38:55 2008 +0100
@@ -275,20 +275,25 @@
   | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
   | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
 
-fun thm_sel name_pos =
-  Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
+fun print_named args =
+  "Facts.Named " ^
     ML_Syntax.print_pair (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position)
-      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name_pos, sel));
+      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) args;
 
-fun thm_antiq kind get = value_antiq kind
-  (Scan.lift (Args.position Args.name :-- thm_sel) >> (fn ((name, _), sel) =>
-    (name, get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)));
+fun thm_antiq kind get get_name = value_antiq kind
+  ((Scan.state >> Context.proof_of) --
+    Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
+  >> (fn (ctxt, thmspec as ((name, _), _)) =>
+      let
+        val _ = get ctxt (Facts.Named thmspec);
+        val thmspec_txt = ML_Syntax.atomic (print_named thmspec);
+      in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ thmspec_txt) end));
 
 in
 
 val _ = add_keywords ["(", ")", "-", ","];
-val _ = thm_antiq "thm" "ProofContext.get_fact_single";
-val _ = thm_antiq "thms" "ProofContext.get_fact";
+val _ = thm_antiq "thm" ProofContext.get_fact_single "ProofContext.get_fact_single";
+val _ = thm_antiq "thms" ProofContext.get_fact "ProofContext.get_fact";
 
 end;