# 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)) =>