# HG changeset patch
# User wenzelm
# Date 1428087137 -7200
# Node ID 86d302846b16d3a8520ed33eb2b8ea4ca450720b
# Parent  fe1d8576b48308470d2838a50ad8133f336c99b6
check wrt. proper context, e.g. relevant for 'experiment' target;

diff -r fe1d8576b483 -r 86d302846b16 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Fri Apr 03 20:23:19 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Fri Apr 03 20:52:17 2015 +0200
@@ -12,6 +12,7 @@
   val del_thm: string -> thm -> Context.generic -> Context.generic
   val add: string -> attribute
   val del: string -> attribute
+  val check: Proof.context -> string * Position.T -> string
   val declare: binding -> string -> local_theory -> string * local_theory
 end;
 
@@ -34,9 +35,11 @@
     then error ("Duplicate declaration of named theorems: " ^ quote name)
     else Symtab.update (name, Thm.full_rules) data);
 
+fun undeclared name = "Undeclared named theorems " ^ quote name;
+
 fun the_entry context name =
   (case Symtab.lookup (Data.get context) name of
-    NONE => error ("Undeclared named theorems " ^ quote name)
+    NONE => error (undeclared name)
   | SOME entry => entry);
 
 fun map_entry name f context =
@@ -57,6 +60,20 @@
 val del = Thm.declaration_attribute o del_thm;
 
 
+(* check *)
+
+fun check ctxt (xname, pos) =
+  let
+    val context = Context.Proof ctxt;
+    val fact_ref = Facts.Named ((xname, Position.none), NONE);
+    fun err () = error (undeclared xname ^ Position.here pos);
+  in
+    (case try (Proof_Context.get_fact_generic context) fact_ref of
+      SOME (SOME name, _) => if can (the_entry context) name then name else err ()
+    | _ => err ())
+  end;
+
+
 (* declaration *)
 
 fun declare binding descr lthy =
@@ -82,11 +99,7 @@
 
 val _ = Theory.setup
   (ML_Antiquotation.inline @{binding named_theorems}
-    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (xname, pos)) =>
-      let
-        val thy = Proof_Context.theory_of ctxt;
-        val name = Global_Theory.check_fact thy (xname, pos);
-        val _ = get ctxt name handle ERROR msg => error (msg ^ Position.here pos);
-      in ML_Syntax.print_string name end)));
+    (Args.context -- Scan.lift (Parse.position Args.name) >>
+      (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
 
 end;