277 fun add_var (key, z) = Vartab.map_default (key, []) (cons z) |
277 fun add_var (key, z) = Vartab.map_default (key, []) (cons z) |
278 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) |
278 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) |
279 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) |
279 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) |
280 | add_type_constraint _ = I |
280 | add_type_constraint _ = I |
281 |
281 |
282 fun fix_atp_variable_name s = |
282 fun fix_atp_variable_name f s = |
283 let |
283 let |
284 fun subscript_name s n = s ^ nat_subscript n |
284 fun subscript_name s n = s ^ nat_subscript n |
285 val s = String.map Char.toLower s |
285 val s = String.map f s |
286 in |
286 in |
287 case space_explode "_" s of |
287 case space_explode "_" s of |
288 [_] => (case take_suffix Char.isDigit (String.explode s) of |
288 [_] => (case take_suffix Char.isDigit (String.explode s) of |
289 (cs1 as _ :: _, cs2 as _ :: _) => |
289 (cs1 as _ :: _, cs2 as _ :: _) => |
290 subscript_name (String.implode cs1) |
290 subscript_name (String.implode cs1) |
347 | NONE => |
347 | NONE => |
348 case strip_prefix_and_undo_ascii schematic_var_prefix a of |
348 case strip_prefix_and_undo_ascii schematic_var_prefix a of |
349 SOME b => Var ((b, 0), T) |
349 SOME b => Var ((b, 0), T) |
350 | NONE => |
350 | NONE => |
351 if is_tptp_variable a then |
351 if is_tptp_variable a then |
352 Var ((fix_atp_variable_name a, 0), T) |
352 Var ((fix_atp_variable_name Char.toLower a, 0), T) |
353 else |
353 else |
354 raise Fail ("Unexpected constant: " ^ quote a) |
354 (* Skolem constants? *) |
|
355 Var ((fix_atp_variable_name Char.toUpper a, 0), T) |
355 in list_comb (t, ts) end |
356 in list_comb (t, ts) end |
356 in aux (SOME HOLogic.boolT) [] end |
357 in aux (SOME HOLogic.boolT) [] end |
357 |
358 |
358 fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = |
359 fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = |
359 if String.isPrefix class_prefix s then |
360 if String.isPrefix class_prefix s then |