--- 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