# HG changeset patch
# User wenzelm
# Date 1427813232 -7200
# Node ID 6292f1f5ffae487c35805f74fa7cbd2fe582a0da
# Parent  05362c246a6491c337b35725a424a491e1842d28
tuned;

diff -r 05362c246a64 -r 6292f1f5ffae src/Pure/Tools/named_theorems.ML
--- 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