# HG changeset patch
# User paulson
# Date 832930924 -7200
# Node ID 69b93ffc29ec93e2a12f60e2cf8763725f4212f3
# Parent  fb07e359b59f90d68f7c5fa9d1655126fa2704de
Augmented comment about conversion to clauses

diff -r fb07e359b59f -r 69b93ffc29ec src/HOL/ex/meson.ML
--- 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,[])));