--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 00:49:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 00:49:38 2010 +0200
@@ -246,18 +246,18 @@
constrained by information from type literals, or by type inference. *)
fun type_from_fo_term tfrees (u as ATerm (a, us)) =
let val Ts = map (type_from_fo_term tfrees) us in
- case strip_prefix_and_undo_ascii type_const_prefix a of
+ case strip_prefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise FO_TERM [u] (* only "tconst"s have type arguments *)
- else case strip_prefix_and_undo_ascii tfree_prefix a of
+ else case strip_prefix_and_unascii tfree_prefix a of
SOME b =>
let val s = "'" ^ b in
TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
end
| NONE =>
- case strip_prefix_and_undo_ascii tvar_prefix a of
+ case strip_prefix_and_unascii tvar_prefix a of
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
| NONE =>
(* Variable from the ATP, say "X1" *)
@@ -267,7 +267,7 @@
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
- case (strip_prefix_and_undo_ascii class_prefix a,
+ case (strip_prefix_and_unascii class_prefix a,
map (type_from_fo_term tfrees) us) of
(SOME b, [T]) => (pos, b, T)
| _ => raise FO_TERM [u]
@@ -309,7 +309,7 @@
[typ_u, term_u] =>
aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
| _ => raise FO_TERM us
- else case strip_prefix_and_undo_ascii const_prefix a of
+ else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
map (aux NONE []) us)
@@ -341,10 +341,10 @@
val ts = map (aux NONE []) (us @ extra_us)
val T = map fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_undo_ascii fixed_var_prefix a of
+ case strip_prefix_and_unascii fixed_var_prefix a of
SOME b => Free (b, T)
| NONE =>
- case strip_prefix_and_undo_ascii schematic_var_prefix a of
+ case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
if is_tptp_variable a then
@@ -575,7 +575,7 @@
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
if tag = "cnf" orelse tag = "fof" then
- (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
+ (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
SOME name =>
if member (op =) rest "file" then
SOME (name, is_true_for axiom_names name)