tuned;

--- a/src/Pure/Tools/named_theorems.ML	Tue Mar 31 16:43:49 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Tue Mar 31 16:47:12 2015 +0200
@@ -61,7 +61,7 @@
 
 fun declare binding descr lthy =
   let
-    val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding;
+    val name = Local_Theory.full_name lthy binding;
     val description =
       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
     val lthy' = lthy