diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/symbols/DerivedDeclaration.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/symbols/DerivedDeclaration.scala
index ec69b5a2d7..a2d802f47e 100644
--- a/src/mmt-api/src/main/info/kwarc/mmt/api/symbols/DerivedDeclaration.scala
+++ b/src/mmt-api/src/main/info/kwarc/mmt/api/symbols/DerivedDeclaration.scala
@@ -189,6 +189,9 @@ class BoundTheoryParameters(id : String, pi : GlobalName, lambda : GlobalName, a
       case tc: TermContainer => tc.get.getOrElse {
         throw GetError("")
       }
+      case mc : MPathContainer => mc.get.getOrElse {
+        throw GetError("")
+      }
       case _ =>
         throw GetError("")
     }
diff --git a/src/mmt-metamath/src/info/kwarc/mmt/metamath/LFTranslator.scala b/src/mmt-metamath/src/info/kwarc/mmt/metamath/LFTranslator.scala
index 6e4fb43d9d..78a3f22787 100644
--- a/src/mmt-metamath/src/info/kwarc/mmt/metamath/LFTranslator.scala
+++ b/src/mmt-metamath/src/info/kwarc/mmt/metamath/LFTranslator.scala
@@ -4,8 +4,9 @@ import scala.collection.mutable.HashMap
 import scala.collection.mutable.Stack
 import scala.collection.mutable.TreeSet
 import org.metamath.scala._
-import info.kwarc.mmt.api.LocalName
+import info.kwarc.mmt.api._
 import info.kwarc.mmt.api.archives.BuildTask
+import info.kwarc.mmt.api.checking.{Checker, CheckingEnvironment, RelationHandler}
 import info.kwarc.mmt.api.documents.{Document, MRef}
 import info.kwarc.mmt.api.frontend.Controller
 import info.kwarc.mmt.api.frontend.Logger
@@ -17,35 +18,39 @@ import info.kwarc.mmt.api.objects.OMV
 import info.kwarc.mmt.api.objects.Term
 import info.kwarc.mmt.api.opaque.OpaqueText
 import info.kwarc.mmt.api.opaque.StringFragment
-import info.kwarc.mmt.api.symbols
 import info.kwarc.mmt.lf.Apply
 import info.kwarc.mmt.lf.Arrow
 import info.kwarc.mmt.lf.Lambda
 import info.kwarc.mmt.lf.Pi
-import info.kwarc.mmt.lf.LF
 
 class LFTranslator(val controller: Controller, bt: BuildTask, index: Document => Unit) extends Logger {
   def logPrefix = "mm-omdoc"
   protected def report = controller.report
 
-  val path = bt.narrationDPath.^!.^!
+  val path = bt.narrationDPath
 
   def addDatabase(db: Database): Document = {
     val mod = Metamath.setmm
     val doc = new Document(path, root = true)
     controller add doc
-    val theory = new DeclaredTheory(path, mod.name, Some(LF.theoryPath), Context.empty)
+    val theory = new DeclaredTheory(mod.doc, mod.name, Some(Metamath.prelude))
     controller add theory
     controller add MRef(doc.path, theory.path)
     val tr = new LFDBTranslator()(db)
-    db.decls foreach {
+    // TODO restricted to the first 1000 constants for inspection
+    val consts = db.decls.filter{case c: Comment => false case _ => true}
+    consts/*.dropRight(consts.length - 1000)*/ foreach {
       case a: Assert if a.syntax || a.typecode.id == "|-" =>
-        controller add symbols.Constant(OMMOD(mod), LocalName(a.label), Nil,
+        controller add symbols.Constant(theory.toTerm, LocalName(a.label), Nil,
           Some(tr.translateAssert(a)), tr.translateProof(a), None)
       case c: Comment =>
-        controller add new OpaqueText(mod.toDPath, List(StringFragment(c.text)))
+        controller add new OpaqueText(theory.asDocument.path, List(StringFragment(c.text)))
       case _ =>
     }
+    val checker = controller.extman.get(classOf[Checker], "mmt").getOrElse {
+      throw GeneralError(s"no MMT checker found")
+    }
+    checker(theory)(new CheckingEnvironment(new ErrorLogger(report), RelationHandler.ignore))
     doc
   }
 }
@@ -53,7 +58,7 @@ class LFTranslator(val controller: Controller, bt: BuildTask, index: Document =>
 class LFDBTranslator(implicit db: Database) {
   val boundVars = new HashMap[Assert, Array[Option[Array[Byte]]]]
   val syntaxToDefn = new HashMap[Assert, Assert]
-  val alignments = new HashMap[Assert, String]
+  val alignments = new HashMap[Assert, GlobalName]
 
   val SET = db.syms("set")
   val DED = db.syms("|-")
@@ -75,20 +80,21 @@ class LFDBTranslator(implicit db: Database) {
     (CAB, Array(None, Some(Array(1, 0)))))
 
   alignments += (
-    (WN, "not"),
-    (WI, "impl"),
-    (WB, "equiv"),
-    (WAL, "forall"),
-    (db.asserts("wa"), "and"),
-    (db.asserts("wo"), "or"),
-    (db.asserts("wtru"), "true"),
-    (db.asserts("wex"), "exists"),
-    (db.asserts("pm3.2i"), "andI"),
-    (db.asserts("simpli"), "andEl"),
-    (db.asserts("simpri"), "andEr"),
-    (db.asserts("orci"), "orIl"),
-    (db.asserts("olci"), "orIr"),
-    (db.asserts("impl"), "_impl"))
+    (WN, Metamath.not),
+    (WI, Metamath.impl),
+    (WB, Metamath.equiv),
+    (WAL, Metamath.setmm ? "forall"),
+    //(db.asserts("wff"), Metamath.wff),
+    (db.asserts("wa"), Metamath.and),
+    (db.asserts("wo"), Metamath.or),
+    (db.asserts("wtru"), Metamath.setmm ? "true"),
+    (db.asserts("wex"), Metamath.setmm ? "exists"),
+    (db.asserts("pm3.2i"), Metamath.setmm ? "andI"),
+    (db.asserts("simpli"), Metamath.setmm ? "andEl"),
+    (db.asserts("simpri"), Metamath.setmm ? "andEr"),
+    (db.asserts("orci"), Metamath.setmm ? "orIl"),
+    (db.asserts("olci"), Metamath.setmm ? "orIr"),
+    (db.asserts("impl"), Metamath.setmm ? "_impl"))
 
   db.decls foreach {
     case a: Assert => processBoundVars(a)
@@ -163,9 +169,10 @@ class LFDBTranslator(implicit db: Database) {
   }
 
   def align(a: Assert): Term =
-    OMS(Metamath.setmm ? alignments.getOrElse(a,a.label))
+    OMS(alignments.getOrElse(a, Metamath.setmm ? a.label))
 
   type DependVars = HashMap[Floating, TreeSet[Floating]]
+
   def getDependVars(stmt: Assert): DependVars = {
     implicit val dependVars = new DependVars
     stmt.hyps foreach {
@@ -187,9 +194,14 @@ class LFDBTranslator(implicit db: Database) {
     dependVars
   }
 
-  val LF_SET = OMS(Metamath.setmm ? "set")
-  def LF_type(s: Statement): Term = OMS(Metamath.setmm ? s.typecode.id)
-  val LF_DED = OMS(Metamath.setmm ? "|-")
+  val LF_SET = OMS(Metamath.set)
+
+  def LF_type(s: Statement): Term = s.typecode.id match {
+    case "wff" => OMS(Metamath.wff)
+    case _ => OMS(Metamath.setmm ? s.typecode.id)
+  }
+
+  val LF_DED = OMS(Metamath.|-)
 
   def LF_var(v: Floating): LocalName = LocalName(v.v.id)
 
@@ -250,7 +262,9 @@ class LFDBTranslator(implicit db: Database) {
           case Some(b) =>
             val needsFree = (b(i) & 2) != 0 ||
               child.zipWithIndex.exists { case (c, j) => b(j) == 3 && c.stmt.typecode != SET }
-            if (needsFree) node match { case HypNode(v: Floating) => Apply(ap, OMV(LF_var(v))) }
+            if (needsFree) node match {
+              case HypNode(v: Floating) => Apply(ap, OMV(LF_var(v)))
+            }
             else ap
           case _ =>
             Apply(ap, child.zip(bv).foldRight(translateTerm(node))((k, t) => k match {
@@ -268,7 +282,9 @@ class LFDBTranslator(implicit db: Database) {
     syntaxToDefn.getOrElse(a, return None).parse match {
       case AssertNode(eq, List(AssertNode(ax, child), p)) =>
         val bv = getBoundVars(a)
-        val t = try { translateTerm(p) } catch {
+        val t = try {
+          translateTerm(p)
+        } catch {
           case e: IllegalArgumentException => return None
         }
         Some(child.zipWithIndex.foldRight(t)((k, t) => k match {
@@ -289,6 +305,7 @@ class LFDBTranslator(implicit db: Database) {
 
   class ScanExpr(free: Option[TreeSet[Floating]] = None)(implicit val dependVars: DependVars) {
     val stack = new Stack[Floating]
+
     def scan(p: ParseTree) {
       p match {
         case HypNode(h: Floating) => free match {
@@ -308,5 +325,4 @@ class LFDBTranslator(implicit db: Database) {
       }
     }
   }
-
 }
\ No newline at end of file
diff --git a/src/mmt-metamath/src/info/kwarc/mmt/metamath/Theory.scala b/src/mmt-metamath/src/info/kwarc/mmt/metamath/Theory.scala
index 5abfba943b..ae08e3185e 100644
--- a/src/mmt-metamath/src/info/kwarc/mmt/metamath/Theory.scala
+++ b/src/mmt-metamath/src/info/kwarc/mmt/metamath/Theory.scala
@@ -8,7 +8,8 @@ import info.kwarc.mmt.api.utils.URI
 object Metamath {
    val _base = DPath(URI.http colon "us.metamath.org")
    val prelude = _base ? "Prelude"
-   
+   val setmm = _base ? "set.mm"
+   /*
    /** Application symbol for $d sets */
    val DV = OMS(prelude ? "DV")
    /** Application symbol for $e (essential) hypotheses */
@@ -33,15 +34,17 @@ object Metamath {
     * </pre>
     */
    val FL = OMS(prelude ? "FL")
+   */
+   def setconst(s: String) = OMS(setmm ? s)
+   def prelconst(s : String) = prelude ? s
    
-   val setmm = _base ? "set.mm"
-
-   def sconst(s: String) = OMS(setmm ? s)
-   
-   val set = sconst("set")
-   val _class = sconst("class")
-   val wff = sconst("wff")
-   val |- = sconst("|-")
-
-   
+   val set = prelconst("set")
+   val _class = prelconst("class")
+   val wff = prelconst("wff")
+   val |- = prelconst("ded")
+   val not = prelconst("not")
+   val impl = prelconst("impl")
+   val equiv = prelconst("equiv")
+   val and = prelconst("and")
+   val or = prelconst("or")
 }
\ No newline at end of file
diff --git a/src/mmt-metamath/src/info/kwarc/mmt/metamath/Translator.scala b/src/mmt-metamath/src/info/kwarc/mmt/metamath/Translator.scala
index ab630d4b55..a11ba2b7cf 100644
--- a/src/mmt-metamath/src/info/kwarc/mmt/metamath/Translator.scala
+++ b/src/mmt-metamath/src/info/kwarc/mmt/metamath/Translator.scala
@@ -13,7 +13,7 @@ import info.kwarc.mmt.api.opaque.StringFragment
 import org.metamath.scala._
 import info.kwarc.mmt.api.MPath
 
-
+/*
 class Translator(val controller: Controller, bt: BuildTask, index: Document => Unit) extends Logger {
   def logPrefix = "mm-omdoc"
   protected def report = controller.report
@@ -46,4 +46,5 @@ class Translator(val controller: Controller, bt: BuildTask, index: Document => U
     }
     controller add theory
   }
-}
\ No newline at end of file
+}
+*/
\ No newline at end of file
diff --git a/src/mmt-pvs/src/info/kwarc/mmt/pvs/Translator.scala b/src/mmt-pvs/src/info/kwarc/mmt/pvs/Translator.scala
index 520d51cfff..3890ef6b05 100644
--- a/src/mmt-pvs/src/info/kwarc/mmt/pvs/Translator.scala
+++ b/src/mmt-pvs/src/info/kwarc/mmt/pvs/Translator.scala
@@ -203,11 +203,12 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
 
   def doFormal(f:FormalParameter) : Unit = f match {
     case formal_type_decl(named,nonempty) =>
+      state.unknowns = 0
       val v = VarDecl(doName(named.named.id),Some(PVSTheory.tp.term),None,None)
       state.th.parameters = state.th.parameters ++ v
       if (nonempty.nonempty_p && nonempty.contains.isDefined) {
         state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
-          PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name)))),
+          state.bindUnknowns(PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name))))),
           None,Some("Assumption")))
       } else if (nonempty.nonempty_p) {
         state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
@@ -223,7 +224,7 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
       state.th.parameters = state.th.parameters ++ v
       if (nonempty.nonempty_p && nonempty.contains.isDefined) {
         state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
-          PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name)))),
+          state.bindUnknowns(PVSTheory.is_nonempty(OMV(v.name),doExprAs(nonempty.contains.get,OMV(v.name))))),
           None,Some("Assumption")))
       } else if (nonempty.nonempty_p) {
         state.th.add(Constant(state.th.toTerm,newName("INTERNAL_Assumption"),Nil,Some(
@@ -263,7 +264,8 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
       case var_decl(id, unnamed, tp) => // Not needed
 
       case tcc_decl(ChainedDecl(NamedDecl(id, _, _), _, _), Assertion(kind, formula)) =>
-        val c = Constant(state.th.toTerm, newName(id + "_TCC"), Nil, Some(PVSTheory.proof(kind, doExprAs(formula, PVSTheory.bool.term))), None,
+        state.unknowns = 0
+        val c = Constant(state.th.toTerm, newName(id + "_TCC"), Nil, Some(state.bind(PVSTheory.proof(kind, doExprAs(formula, PVSTheory.bool.term)))), None,
           Some(if (isAss) "Assumption_TCC" else "TCC"))
         state.th add c
         state.tcc = Some(c)
@@ -283,6 +285,7 @@ class PVSImportTask(val controller: Controller, bt: BuildTask, index: Document =
 
       case formula_decl(ChainedDecl(NamedDecl(id, _, _), _, _), Assertion(kind, form)) =>
         state.vars = Nil
+        state.unknowns = 0
         val phi = doExprAs(form, PVSTheory.bool.term)
         state.th add Constant(state.th.toTerm, newName(id), Nil, Some(state.bind(PVSTheory.proof(kind, phi))), None, if (isAss) Some("Assumption") else None)
 
diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/STeXAnalysis.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/STeXAnalysis.scala
index e9111f0e34..2cb44d1108 100644
--- a/src/mmt-stex/src/info/kwarc/mmt/stex/STeXAnalysis.scala
+++ b/src/mmt-stex/src/info/kwarc/mmt/stex/STeXAnalysis.scala
@@ -150,6 +150,7 @@ trait STeXAnalysis {
     def join(s: STeXStructure) = {
       struct = struct.join(s)
     }
+
     lines.foreach { line =>
       val l = stripComment(line).trim
       val verbIndex = l.indexOf("\\verb")
diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/STeXUtils.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/STeXUtils.scala
index 2a99dd2009..878af1baad 100644
--- a/src/mmt-stex/src/info/kwarc/mmt/stex/STeXUtils.scala
+++ b/src/mmt-stex/src/info/kwarc/mmt/stex/STeXUtils.scala
@@ -57,7 +57,7 @@ object STeXUtils {
   }
 
   def readSourceRebust(f: File): BufferedSource =
-    scala.io.Source.fromFile(f)
+    scala.io.Source.fromFile(f)(Codec.UTF8)
 
   def stripComment(line: String): String = {
     val idx = line.indexOf('%')
diff --git a/src/test/preamble.scala b/src/test/preamble.scala
index 9ca0b2cc04..f7cce0458c 100644
--- a/src/test/preamble.scala
+++ b/src/test/preamble.scala
@@ -50,7 +50,7 @@ abstract class Test(archivepath : String,
   * As an example, here's my default. All test files of mine just extend this:
   */
 abstract class DennisTest(prefixes : String*) extends Test(
-  "/home/raupi/lmh/MathHub",
+  "/home/raupi/lmh/localmh/MathHub",
   prefixes.toList,
   "/home/raupi/lmh/Stuff/Public",
   Some(8080),