src/HOL/Tools/meson.ML

 val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms;
 
 fun make_nnf th = th |> simplify nnf_ss
                      |> check_no_bool |> make_nnf1
 
-(*Pull existential quantifiers (Skolemization)*)
+(*Pull existential quantifiers to front. This accomplishes Skolemization for
+  clauses that arise from a subgoal.*)
 fun skolemize th =
   if not (has_consts ["Ex"] (prop_of th)) then th
   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
                               disj_exD, disj_exD1, disj_exD2])))
     handle THM _ =>

 
 
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
 fun make_clauses ths =
-   (  sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
+    (sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
 
 
 (*Convert a list of clauses to (contrapositive) Horn clauses*)
 fun make_horns ths =
     name_thms "Horn#"