src/HOL/Tools/res_axioms.ML
 changeset 20373 dcb321249aa9 parent 20362 bbff23c3e2ca child 20419 df257a9cf0e9
equal inserted replaced
20372:e42674e0486e 20373:dcb321249aa9
`   239   handle THM _ => [];`
`   239   handle THM _ => [];`
`   240 `
`   240 `
`   241 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.`
`   241 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.`
`   242   It returns a modified theory, unless skolemization fails.*)`
`   242   It returns a modified theory, unless skolemization fails.*)`
`   243 fun skolem thy (name,th) =`
`   243 fun skolem thy (name,th) =`
`   244   let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)`
`   244   let val cname = (case name of "" => gensym "sko_" | s => Sign.base_name s)`
`   245   in Option.map `
`   245   in Option.map `
`   246         (fn nnfth => `
`   246         (fn nnfth => `
`   247           let val (thy',defs) = declare_skofuns cname nnfth thy`
`   247           let val (thy',defs) = declare_skofuns cname nnfth thy`
`   248               val skoths = map skolem_of_def defs`
`   248               val skoths = map skolem_of_def defs`
`   249           in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)`
`   249           in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)`