src/HOL/TPTP/atp_theory_export.ML
changeset 52031 9a9238342963
parent 51998 f732a674db1b
child 52754 d9d90d29860e
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu May 16 13:34:13 2013 +0200
@@ -157,7 +157,7 @@
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val type_enc =
-      type_enc |> type_enc_from_string Non_Strict
+      type_enc |> type_enc_of_string Non_Strict
                |> adjust_type_enc format
     val mono = not (is_type_enc_polymorphic type_enc)
     val facts =