equal
deleted
inserted
replaced
282 (user_ths_cls,local_simpR_cls,local_claR_cls,errs) |
282 (user_ths_cls,local_simpR_cls,local_claR_cls,errs) |
283 end; |
283 end; |
284 |
284 |
285 fun cnf_hyps_thms ctxt = |
285 fun cnf_hyps_thms ctxt = |
286 let val ths = ProofContext.prems_of ctxt |
286 let val ths = ProofContext.prems_of ctxt |
287 val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux ths) |
287 in |
288 in |
288 ResClause.union_all (map ResAxioms.skolem_thm ths) |
289 prems |
|
290 end; |
289 end; |
291 |
290 |
292 (**** clausification ****) |
291 (**** clausification ****) |
293 fun cls_axiom_fol _ _ [] = [] |
292 fun cls_axiom_fol _ _ [] = [] |
294 | cls_axiom_fol name i (tm::tms) = |
293 | cls_axiom_fol name i (tm::tms) = |