src/HOL/TPTP/mash_export.ML

     fun do_fact ((_, stature), th) =
       let
         val name = nickname_of_thm th
         val feats =
           features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] |> map fst
-        val s = encode_str name ^ ": " ^ encode_plain_features (sort_wrt hd feats) ^ "\n"
+        val s = encode_str name ^ ": " ^ encode_unweighted_features (sort_wrt hd feats) ^ "\n"
       in File.append path s end
   in List.app do_fact facts end
 
 val prover_marker = "$a"
 val isar_marker = "$i"

             features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature false
               [prop_of th]
             |> map fst |> sort_wrt hd
           val update =
             "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
-            encode_plain_features nongoal_feats ^ "; " ^ marker ^ " " ^
-            encode_strs deps ^ "\n"
+            encode_unweighted_features nongoal_feats ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
         in query ^ update end
       else
         ""
     val new_facts =
       new_facts |> attach_parents_to_facts old_facts