src/HOL/Tools/Meson/meson.ML
changeset 59171 75ec7271b426
parent 59165 115965966e15
child 59498 50b60f501b05
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Dec 21 22:49:17 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Dec 21 22:49:40 2014 +0100
     1.3 @@ -358,12 +358,6 @@
     1.4      in (th RS spec', ctxt') end
     1.5  end;
     1.6  
     1.7 -(*Used with METAHYPS below. There is one assumption, which gets bound to prem
     1.8 -  and then normalized via function nf. The normal form is given to resolve_tac,
     1.9 -  instantiate a Boolean variable created by resolution with disj_forward. Since
    1.10 -  (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
    1.11 -fun resop nf [prem] = resolve_tac (nf prem) 1;
    1.12 -
    1.13  fun apply_skolem_theorem (th, rls) =
    1.14    let
    1.15      fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
    1.16 @@ -392,10 +386,12 @@
    1.17            | Const (@{const_name HOL.disj}, _) =>
    1.18                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    1.19                  all combinations of converting P, Q to CNF.*)
    1.20 -              let val tac =
    1.21 -                  Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1 THEN
    1.22 -                   (fn st' => st' |> Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1)
    1.23 -              in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    1.24 +              (*There is one assumption, which gets bound to prem and then normalized via
    1.25 +                cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean
    1.26 +                variable created by resolution with disj_forward. Since (cnf_nil prem)
    1.27 +                returns a LIST of theorems, we can backtrack to get all combinations.*)
    1.28 +              let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac (cnf_nil prem) 1) 1
    1.29 +              in  Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths  end
    1.30            | _ => nodups ctxt th :: ths  (*no work to do*)
    1.31        and cnf_nil th = cnf_aux (th, [])
    1.32        val cls =