# HG changeset patch
# User blanchet
# Date 1645538404 -3600
# Node ID 18cd39e55eca17e924067f47128a67d239825a63
# Parent  f12539c8de0cfdd6f06153239a3d1a2321592c8f
have Sledgehammer honor 'smt_nat_as_int' option

diff -r f12539c8de0c -r 18cd39e55eca src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Feb 22 12:45:14 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Feb 22 15:00:04 2022 +0100
@@ -409,8 +409,9 @@
     val long = Thm.get_name_hint th
     val short = Long_Name.base_name long
   in
-    if Thm.eq_thm_prop (th, singleton (Attrib.eval_thms ctxt) (Facts.named short, [])) then short
-    else long
+    (case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of
+      SOME th' => if Thm.eq_thm_prop (th, th') then short else long
+    | _ => long)
   end
 
 val map_prod = Ctr_Sugar_Util.map_prod
diff -r f12539c8de0c -r 18cd39e55eca src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Feb 22 12:45:14 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Feb 22 15:00:04 2022 +0100
@@ -75,12 +75,16 @@
     val run_timeout = slice_timeout slices timeout
     val (higher_order, nat_as_int) =
       (case type_enc of
-        SOME s =>  (String.isSubstring "native_higher" s, String.isSubstring "arith" s)
-      | NONE => (false, false))
+        SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s))
+      | NONE => (NONE, NONE))
     fun repair_context ctxt = ctxt
       |> Context.proof_map (SMT_Config.select_solver name)
-      |> Config.put SMT_Config.higher_order higher_order
-      |> Config.put SMT_Config.nat_as_int nat_as_int
+      |> (case higher_order of
+           SOME higher_order => Config.put SMT_Config.higher_order higher_order
+         | NONE => I)
+      |> (case nat_as_int of
+           SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int
+         | NONE => I)
       |> (if overlord then
             Config.put SMT_Config.debug_files
               (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))