src/HOL/Tools/Meson/meson.ML

       val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
       val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
     in (th RS spec', ctxt') end
 end;
 
-(*Used with METAHYPS below. There is one assumption, which gets bound to prem
-  and then normalized via function nf. The normal form is given to resolve_tac,
-  instantiate a Boolean variable created by resolution with disj_forward. Since
-  (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
-fun resop nf [prem] = resolve_tac (nf prem) 1;
-
 fun apply_skolem_theorem (th, rls) =
   let
     fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
       | tryall (rl :: rls) =
         first_order_resolve th rl handle THM _ => tryall rls

               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
           | Const (@{const_name HOL.disj}, _) =>
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
-              let val tac =
-                  Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1 THEN
-                   (fn st' => st' |> Misc_Legacy.METAHYPS ctxt (resop cnf_nil) 1)
-              in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
+              (*There is one assumption, which gets bound to prem and then normalized via
+                cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean
+                variable created by resolution with disj_forward. Since (cnf_nil prem)
+                returns a LIST of theorems, we can backtrack to get all combinations.*)
+              let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac (cnf_nil prem) 1) 1
+              in  Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths  end
           | _ => nodups ctxt th :: ths  (*no work to do*)
       and cnf_nil th = cnf_aux (th, [])
       val cls =
         if has_too_many_clauses ctxt (concl_of th) then
           (trace_msg ctxt (fn () =>