src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42569 5737947e4c77
parent 42568 7b9801a34836
child 42570 77f94ac04f32
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -233,8 +233,8 @@
     1.4                  "c_False" => (tptp_false, s')
     1.5                | "c_True" => (tptp_true, s')
     1.6                | _ => name, [])
     1.7 -            else
     1.8 -              (proxy_base |>> prefix const_prefix, ty_args)
     1.9 +           else
    1.10 +             (proxy_base |>> prefix const_prefix, ty_args)
    1.11            | NONE => (name, ty_args))
    1.12          |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
    1.13        | aux _ tm = tm
    1.14 @@ -477,7 +477,7 @@
    1.15          (case strip_prefix_and_unascii const_prefix s of
    1.16             NONE => (name, ty_args)
    1.17           | SOME s'' =>
    1.18 -           let val s'' = invert_const s'' in
    1.19 +           let val s'' = safe_invert_const s'' in
    1.20               case type_arg_policy type_sys s'' of
    1.21                 No_Type_Args => (name, [])
    1.22               | Mangled_Types => (mangled_const_name ty_args name, [])
    1.23 @@ -682,7 +682,7 @@
    1.24    | NONE =>
    1.25      case strip_prefix_and_unascii const_prefix s of
    1.26        SOME s =>
    1.27 -      let val s = s |> unmangled_const_name |> invert_const in
    1.28 +      let val s = s |> unmangled_const_name |> safe_invert_const in
    1.29          if s = predicator_base then 1
    1.30          else if s = explicit_app_base then 2
    1.31          else if s = type_pred_base then 1