# HG changeset patch
# User wenzelm
# Date 1256494775 -3600
# Node ID 3012726e99296429b98db4aaed287ce4845d473d
# Parent  853493e5d5d40a6b0005b2cb393092b87b72736a
LocalTheory.naming_of;

diff -r 853493e5d5d4 -r 3012726e9929 src/Pure/simplifier.ML
--- 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;