# HG changeset patch
# User blanchet
# Date 1304549516 -7200
# Node ID e38590764c34fc9182579437c97a488a3bbbe2bf
# Parent  097a61baeca9869916dfa052c14194f36b2b06f3
versions of ! and ? for the ASCII-challenged Mirabelle

diff -r 097a61baeca9 -r e38590764c34 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 00:22:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 00:51:56 2011 +0200
@@ -100,6 +100,9 @@
   Preds of polymorphism * type_level |
   Tags of polymorphism * type_level
 
+fun try_unsuffixes ss s =
+  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
+
 fun type_sys_from_string s =
   (case try (unprefix "mangled_") s of
      SOME s => (Mangled_Monomorphic, s)
@@ -108,10 +111,11 @@
        SOME s => (Monomorphic, s)
      | NONE => (Polymorphic, s))
   ||> (fn s =>
-          case try (unsuffix "?") s of
+          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
+          case try_unsuffixes ["?", "_query"] s of
             SOME s => (Nonmonotonic_Types, s)
           | NONE =>
-            case try (unsuffix "!") s of
+            case try_unsuffixes ["!", "_bang"] s of
               SOME s => (Finite_Types, s)
             | NONE => (All_Types, s))
   |> (fn (polymorphism, (level, core)) =>