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