230 | ATerm ((s, tys), us) => |
230 | ATerm ((s, tys), us) => |
231 if s = "" |
231 if s = "" |
232 then error "Isar proof reconstruction failed because the ATP proof \ |
232 then error "Isar proof reconstruction failed because the ATP proof \ |
233 \contains unparsable material." |
233 \contains unparsable material." |
234 else if s = tptp_equal then |
234 else if s = tptp_equal then |
235 let val ts = map (do_term NONE) us in |
235 let |
236 if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then |
236 val ts = map (do_term NONE) us |
237 @{const True} |
237 fun equal_term ts = |
|
238 list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts) |
|
239 in |
|
240 if textual then |
|
241 (case ts of |
|
242 [fst, lst] => |
|
243 if loose_aconv (fst, lst) then |
|
244 @{const True} |
|
245 else if Term.aconv_untyped (lst, @{const True}) then |
|
246 fst |
|
247 else if Term.aconv_untyped (fst, @{const True}) then |
|
248 lst |
|
249 else |
|
250 equal_term ts |
|
251 | _ => equal_term ts) |
238 else |
252 else |
239 list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts) |
253 equal_term ts |
240 end |
254 end |
241 else if not (null us) then |
255 else if not (null us) then |
242 let |
256 let |
243 val args = List.map (do_term NONE) us |
257 val args = List.map (do_term NONE) us |
244 val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T) |
258 val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T) |