# HG changeset patch
# User paulson
# Date 1156781732 -7200
# Node ID d9606c64bc23b35223b775b541525b5b5762e3ad
# Parent  56ef2dfc41d63cefbc6f056e7c9dbe6cdd19641e
tidied

diff -r 56ef2dfc41d6 -r d9606c64bc23 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Aug 28 16:10:44 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Aug 28 18:15:32 2006 +0200
@@ -240,8 +240,7 @@
 fun list_cabs ([] ,     t) = t
   | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
 
-(*FIXME DELETE*)
-fun check_eta ct = 
+fun assert_eta_free ct = 
   let val t = term_of ct 
   in if (t aconv Envir.eta_contract t) then ()  
      else error ("Eta redex in term: " ^ string_of_cterm ct)
@@ -253,7 +252,7 @@
   let fun abstract thy ct = case term_of ct of
           Abs (_,T,u) =>
 	    let val cname = gensym "abs_"
-	        val _ = check_eta ct;
+	        val _ = assert_eta_free ct;
 		val (cv,cta) = Thm.dest_abs NONE ct
 		val v = (#1 o dest_Free o term_of) cv
 		val (u'_th,defs) = abstract thy cta
@@ -292,7 +291,7 @@
       fun abstract vs ct = case term_of ct of
           Abs (_,T,u) =>
 	    let val (cv,cta) = Thm.dest_abs NONE ct
-	        val _ = check_eta ct;
+	        val _ = assert_eta_free ct;
 		val v = (#1 o dest_Free o term_of) cv
 		val (u'_th,defs) = abstract (v::vs) cta
                 val cu' = crhs u'_th
@@ -384,7 +383,7 @@
 	  val (thy'', ths') = declare_abstract' (thy', ths)
       in  (thy'', th_defs @ ths')  end;
 
-(*FIXME DELETE*)
+(*FIXME DELETE if we decide to switch to abstractions*)
 fun declare_abstract (thy, ths) =
   if abstract_lambdas then declare_abstract' (thy, ths)
   else (thy, map eta_conversion_rule ths);
diff -r 56ef2dfc41d6 -r d9606c64bc23 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Mon Aug 28 16:10:44 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Mon Aug 28 18:15:32 2006 +0200
@@ -474,13 +474,10 @@
     end;
 
 
-fun make_conjecture_clause n thm = 
-    make_clause(n,"conjecture",Conjecture,thm,true);
- 
-
 fun make_conjecture_clauses_aux _ [] = []
-  | make_conjecture_clauses_aux n (t::ts) =
-    make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts;
+  | make_conjecture_clauses_aux n (th::ths) =
+      make_clause(n,"conjecture",Conjecture,th,true) ::
+      make_conjecture_clauses_aux (n+1) ths;
 
 val make_conjecture_clauses = make_conjecture_clauses_aux 0;