LocalTheory.naming_of;

--- a/src/Pure/simplifier.ML	Sun Oct 25 19:19:29 2009 +0100
+++ b/src/Pure/simplifier.ML	Sun Oct 25 19:19:35 2009 +0100
@@ -177,9 +177,9 @@
 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
   let
     val b = Binding.name name;
-    val naming = LocalTheory.full_naming lthy;
+    val naming = LocalTheory.naming_of lthy;
     val simproc = make_simproc
-      {name = LocalTheory.full_name lthy b,
+      {name = Name_Space.full_name naming b,
        lhss =
         let
           val lhss' = prep lthy lhss;