diff -r 17160e0a60b6 -r fc9ba6fe367f src/Pure/term.scala
--- a/src/Pure/term.scala	Thu Aug 15 16:38:55 2019 +0200
+++ b/src/Pure/term.scala	Thu Aug 15 16:57:09 2019 +0200
@@ -58,7 +58,8 @@
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class OfClass(typ: Typ, cls: String) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
-  case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof
+  case class PThm(serial: Long, theory_name: String, pseudo_name: String, types: List[Typ])
+    extends Proof
 
 
   /* Pure logic */
@@ -184,8 +185,8 @@
               case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
               case Oracle(name, prop, types) =>
                 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
-              case PThm(serial, name, types) =>
-                store(PThm(serial, cache_string(name), cache_typs(types)))
+              case PThm(serial, theory_name, name, types) =>
+                store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
             }
         }
       }