# HG changeset patch
# User blanchet
# Date 1277460924 -7200
# Node ID 6034aac6514382caecbd1da2b39945e2ec4ec6ae
# Parent  2dc53a9f69c93d0ea3cbc52e7c1808f073703c25
eta-expand

diff -r 2dc53a9f69c9 -r 6034aac65143 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:08:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:15:24 2010 +0200
@@ -620,7 +620,7 @@
 fun count_literal (Literal (_, t)) = count_combterm t
 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
 
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
+fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
   #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)