Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper parsing of type encoding;
authordesharna
Thu, 26 Nov 2020 18:45:19 +0100
changeset 72915 e05b77e1ab21
parent 72914 224eacc4d579
child 72916 999b07bfd886
proper parsing of type encoding; tuned naming
src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/ATP/atp_problem_generate.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Nov 26 18:06:36 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Nov 26 18:45:19 2020 +0100
@@ -33,7 +33,7 @@
 
   datatype fool = Without_FOOL | With_FOOL
   datatype polymorphism = Monomorphic | Polymorphic
-  datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+  datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
 
   datatype atp_format =
     CNF |
@@ -193,7 +193,7 @@
 
 datatype fool = Without_FOOL | With_FOOL
 datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
 
 datatype atp_format =
   CNF |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 26 18:06:36 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 26 18:45:19 2020 +0100
@@ -654,11 +654,11 @@
           | (_, Undercover_Types) => raise Same.SAME
           | (Mangled_Monomorphic, _) =>
             if is_type_level_uniform level then
-              Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level)
+              Native (Higher_Order THF_With_Choice, fool, Mangled_Monomorphic, level)
             else
               raise Same.SAME
            | (poly as Raw_Polymorphic _, All_Types) =>
-             Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types)
+             Native (Higher_Order THF_With_Choice, fool, poly, All_Types)
            | _ => raise Same.SAME))
       end
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Nov 26 18:06:36 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Nov 26 18:45:19 2020 +0100
@@ -296,7 +296,7 @@
        val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
        val (format, enc) =
          if modern then
-           (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher")
+           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher")
          else
            (TFF (Without_FOOL, Monomorphic), "mono_native")
      in
isabelle