--- a/src/HOL/ex/meson.ML Thu May 23 15:17:23 1996 +0200
+++ b/src/HOL/ex/meson.ML Fri May 24 11:42:04 1996 +0200
@@ -317,7 +317,8 @@
(*Convert all suitable free variables to schematic variables*)
fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
-(*Make clauses from a list of theorems. These are HOL disjunctions.*)
+(*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,[])));