--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200
@@ -233,8 +233,8 @@
"c_False" => (tptp_false, s')
| "c_True" => (tptp_true, s')
| _ => name, [])
- else
- (proxy_base |>> prefix const_prefix, ty_args)
+ else
+ (proxy_base |>> prefix const_prefix, ty_args)
| NONE => (name, ty_args))
|> (fn (name, ty_args) => CombConst (name, ty, ty_args))
| aux _ tm = tm
@@ -477,7 +477,7 @@
(case strip_prefix_and_unascii const_prefix s of
NONE => (name, ty_args)
| SOME s'' =>
- let val s'' = invert_const s'' in
+ let val s'' = safe_invert_const s'' in
case type_arg_policy type_sys s'' of
No_Type_Args => (name, [])
| Mangled_Types => (mangled_const_name ty_args name, [])
@@ -682,7 +682,7 @@
| NONE =>
case strip_prefix_and_unascii const_prefix s of
SOME s =>
- let val s = s |> unmangled_const_name |> invert_const in
+ let val s = s |> unmangled_const_name |> safe_invert_const in
if s = predicator_base then 1
else if s = explicit_app_base then 2
else if s = type_pred_base then 1