diff -r f9d085c2625c -r 05f57309170c src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -134,16 +134,16 @@
     fun prf_of [] (Bound i) = PBound i
       | prf_of Ts (Const (s, Type ("proof", _))) =
           change_type (if ty then SOME Ts else NONE)
-            (case NameSpace.unpack s of
+            (case NameSpace.explode s of
                "axm" :: xs =>
                  let
-                   val name = NameSpace.pack xs;
+                   val name = NameSpace.implode xs;
                    val prop = (case AList.lookup (op =) axms name of
                        SOME prop => prop
                      | NONE => error ("Unknown axiom " ^ quote name))
                  in PAxm (name, prop, NONE) end
              | "thm" :: xs =>
-                 let val name = NameSpace.pack xs;
+                 let val name = NameSpace.implode xs;
                  in (case AList.lookup (op =) thms name of
                      SOME thm => fst (strip_combt (Thm.proof_of thm))
                    | NONE => (case Symtab.lookup tab name of