src/Pure/pure_thy.ML
changeset 33095 bbd52d2f8696
parent 32786 f1ac4b515af9
child 33167 f02b804305d6
--- a/src/Pure/pure_thy.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/pure_thy.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -146,7 +146,7 @@
   else
     let
       val naming = Sign.naming_of thy;
-      val name = NameSpace.full_name naming b;
+      val name = Name_Space.full_name naming b;
       val (thy', thms') =
         register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
       val thms'' = map (Thm.transfer thy') thms';