# HG changeset patch
# User paulson
# Date 1116606910 -7200
# Node ID 4ae42d8f2fea4907d20600fcc49178d31f98d898
# Parent  237aafbdb1f4ef888c66a2f950adfa21e2a63883
bug fixes for clause form transformation

diff -r 237aafbdb1f4 -r 4ae42d8f2fea src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri May 20 18:34:14 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Fri May 20 18:35:10 2005 +0200
@@ -158,7 +158,11 @@
      handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths))
   end;
 
-fun make_cnf skoths th = cnf skoths (th, []);
+(*Convert all suitable free variables to schematic variables, 
+  but don't discharge assumptions.*)
+fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
+
+fun make_cnf skoths th = map generalize (cnf skoths (th, []));
 
 
 (**** Removal of duplicate literals ****)
@@ -207,10 +211,8 @@
 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
 
 (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)
-fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths);
-
-(*Convert all suitable free variables to schematic variables*)
-fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
+fun sort_clauses ths =
+    sort (make_ord fewerlits) (List.filter (not o is_taut) ths);
 
 (*True if the given type contains bool anywhere*)
 fun has_bool (Type("bool",_)) = true
diff -r 237aafbdb1f4 -r 4ae42d8f2fea src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri May 20 18:34:14 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Fri May 20 18:35:10 2005 +0200
@@ -9,7 +9,7 @@
   sig
   exception ELIMR2FOL of string
   val elimRule_tac : thm -> Tactical.tactic
-  val elimR2Fol : thm -> Term.term
+  val elimR2Fol : thm -> term
   val transform_elim : thm -> thm
   
   val clausify_axiom : thm -> ResClause.clause list
@@ -20,8 +20,7 @@
   val clausify_classical_rules_thy : theory -> ResClause.clause list list * thm list
   val cnf_simpset_rules_thy : theory -> thm list list * thm list
   val clausify_simpset_rules_thy : theory -> ResClause.clause list list * thm list
-  val rm_Eps 
-  : (Term.term * Term.term) list -> thm list -> Term.term list
+  val rm_Eps : (term * term) list -> thm list -> term list
   val claset_rules_of_thy : theory -> (string * thm) list
   val simpset_rules_of_thy : theory -> (string * thm) list
   val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list
@@ -112,7 +111,7 @@
     end;
 
     
-(* convert an elim rule into an equivalent formula, of type Term.term. *)
+(* convert an elim rule into an equivalent formula, of type term. *)
 fun elimR2Fol elimR = 
     let val elimR' = Drule.freeze_all elimR
 	val (prems,concl) = (prems_of elimR', concl_of elimR')
@@ -196,19 +195,22 @@
   let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, thy) =
 	    (*Existential: declare a Skolem function, then insert into body and continue*)
 	    let val cname = s ^ "_" ^ Int.toString n
-		val args = term_frees xtp
+		val args = term_frees xtp  (*get the formal parameter list*)
 		val Ts = map type_of args
 		val cT = Ts ---> T
 		val c = Const(NameSpace.append (PureThy.get_name thy) cname, cT)
+		        (*Generates a compound constant name in the given theory*)
 		val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
+		        (*Forms a lambda-abstraction over the formal parameters*)
 		val def = equals cT $ c $ rhs
 		val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
+		           (*Theory is augmented with the constant, then its def*)
 		val thy'' = Theory.add_defs_i false [(cname ^ "_def", def)] thy'
 	    in dec_sko (subst_bound (list_comb(c,args), p)) (n+1, thy'') end
 	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thy) =
-	    (*Universal: insert a free variable into body and continue*)
+	    (*Universal quant: insert a free variable into body and continue*)
 	    let val fname = variant (add_term_names (p,[])) a
-	    in dec_sko (subst_bound (Free(fname,T), p)) (n+1, thy) end
+	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thy) end
 	| dec_sko (Const ("op &", _) $ p $ q) nthy = 
 	    dec_sko q (dec_sko p nthy)
 	| dec_sko (Const ("op |", _) $ p $ q) nthy =