Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_translate.ML
changeset 45303 bd03b08161ac
parent 45301 866b075aa99b
child 45304 e6901aa86a9e 
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Oct 29 13:15:58 2011 +0200
@@ -640,7 +640,7 @@
   | adjust_type_enc (THF _) type_enc = type_enc
   | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
     Simple_Types (First_Order, Mangled_Monomorphic, level)
-  | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) =
+  | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
     Simple_Types (First_Order, Mangled_Monomorphic, level)
   | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
     Simple_Types (First_Order, poly, level)
@@ -2365,6 +2365,7 @@
           | FOF => I
           | TFF (_, TPTP_Implicit) => I
           | THF (_, TPTP_Implicit, _) => I
+          | DFG DFG_Unsorted => I
           | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
                                                         implicit_declsN)
     val (problem, pool) = problem |> nice_atp_problem readable_names
isabelle