# HG changeset patch
# User blanchet
# Date 1341502273 -7200
# Node ID 4b93fc861cfa7051cf4bc7e454f7a143bcbd76b1
# Parent  24579c5683dd1c0869dd6b22361a8fe86290adae
make SML/NJ happy + tuning

diff -r 24579c5683dd -r 4b93fc861cfa src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 05 16:30:50 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 05 17:31:13 2012 +0200
@@ -1140,13 +1140,10 @@
   in intro true [] end
 
 fun mangle_type_args_in_const type_enc (name as (s, _)) T_args =
-  case unprefix_and_unascii const_prefix s of
-    NONE => (name, T_args)
-  | SOME s'' =>
-    if is_type_enc_mangling type_enc then
-      (mangled_const_name type_enc T_args name, [])
-    else
-      (name, T_args)
+  if String.isPrefix const_prefix s andalso is_type_enc_mangling type_enc then
+    (mangled_const_name type_enc T_args name, [])
+  else
+    (name, T_args)
 fun mangle_type_args_in_iterm type_enc =
   if is_type_enc_mangling type_enc then
     let
@@ -1380,7 +1377,7 @@
    models in first-order logic (via Löwenheim-Skolem). *)
 
 fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
-                             maybe_nonmono_Ts, ...}
+                             maybe_nonmono_Ts}
                        (Nonmono_Types (strictness, _)) T =
     let val thy = Proof_Context.theory_of ctxt in
       (exists (type_intersect thy T) maybe_nonmono_Ts andalso