this should work

Author: digama0

src/portableML/mosml/MLSYSPortable.sml

@@ -48,6 +48,4 @@ fun syncref init =
     }
   end
 
-fun export (_: string * 'a) = raise Fail "export not supported on mosml"
-
 end (* struct *)

src/portableML/poly/MLSYSPortable.sml

@@ -76,12 +76,4 @@ fun syncref init =
      upd = fn f => Synchronized.change_result v f}
   end
 
-fun export (file, x: 'a) = let
-  val _ = PolyML.shareCommonData x
-  val body = PolyML.exportSmall x
-  val ostream = BinIO.openOut file
-  val () = BinIO.output (ostream, body)
-  val () = BinIO.closeOut ostream
-in () end
-
 end

src/tracing/yes/Tracing.sml

@@ -3,10 +3,18 @@ struct
 
 open TheoryPP
 
+fun export (file, x: 'a) = let
+  val _ = PolyML.shareCommonData x
+  val body = PolyML.exportSmall x
+  val ostream = BinIO.openOut file
+  val () = BinIO.output (ostream, body)
+  val () = BinIO.closeOut ostream
+in () end
+
 fun trace_theory name
     ({theory,parents,types,constants,axioms,definitions,theorems,mldeps,...}: struct_info_record) = let
   val file = concat[".holobjs/",name,".tr"]
-  val () = Portable.export(file, (theory,parents,types,constants,axioms,definitions,theorems,mldeps))
+  val () = export(file, (theory,parents,types,constants,axioms,definitions,theorems,mldeps))
   val _ = Unix.execute ("/usr/bin/gzip", ["-f", file])
 in () end
 

tools/sequences/kernel

@@ -20,7 +20,8 @@ src/prekernel
 src/thm
 (stdknl)src/tracing/no
 (expk)src/tracing/no
-(trknl)src/tracing/yes
+[poly](trknl)src/tracing/yes
+[mosml](trknl)src/tracing/no
 (otknl)src/tracing/no
 src/postkernel
 # these three directories are required to even run hol.bare.unquote