equal
deleted
inserted
replaced
483 case Symtab.lookup (!clause_cache) name of |
483 case Symtab.lookup (!clause_cache) name of |
484 NONE => |
484 NONE => |
485 (case skolem thy (name, Thm.transfer thy th) of |
485 (case skolem thy (name, Thm.transfer thy th) of |
486 NONE => ([th],thy) |
486 NONE => ([th],thy) |
487 | SOME (thy',cls) => |
487 | SOME (thy',cls) => |
488 let val cls = map Drule.local_standard cls |
488 let val cls = map Goal.close_result cls |
489 in |
489 in |
490 if null cls then warning ("skolem_cache: empty clause set for " ^ name) |
490 if null cls then warning ("skolem_cache: empty clause set for " ^ name) |
491 else (); |
491 else (); |
492 change clause_cache (Symtab.update (name, (th, cls))); |
492 change clause_cache (Symtab.update (name, (th, cls))); |
493 (cls,thy') |
493 (cls,thy') |
504 (Output.debug ("cnf_axiom called, theorem name = " ^ name); |
504 (Output.debug ("cnf_axiom called, theorem name = " ^ name); |
505 case name of |
505 case name of |
506 "" => skolem_thm th (*no name, so can't cache*) |
506 "" => skolem_thm th (*no name, so can't cache*) |
507 | s => case Symtab.lookup (!clause_cache) s of |
507 | s => case Symtab.lookup (!clause_cache) s of |
508 NONE => |
508 NONE => |
509 let val cls = map Drule.local_standard (skolem_thm th) |
509 let val cls = map Goal.close_result (skolem_thm th) |
510 in Output.debug "inserted into cache"; |
510 in Output.debug "inserted into cache"; |
511 change clause_cache (Symtab.update (s, (th, cls))); cls |
511 change clause_cache (Symtab.update (s, (th, cls))); cls |
512 end |
512 end |
513 | SOME(th',cls) => |
513 | SOME(th',cls) => |
514 if eq_thm(th,th') then cls |
514 if eq_thm(th,th') then cls |