src/HOL/Tools/res_hol_clause.ML
changeset 27178 c8ddb3000743
parent 25243 78f8aaa27493
child 27187 17b63e145986
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 16:42:00 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 18:54:29 2008 +0200
     1.3 @@ -395,7 +395,8 @@
     1.4    if axiom_name mem_string user_lemmas then foldl count_literal ct literals
     1.5    else ct;
     1.6  
     1.7 -val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
     1.8 +fun cnf_helper_thms thy =
     1.9 +  ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
    1.10  
    1.11  fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
    1.12    if isFO then []  (*first-order*)
    1.13 @@ -404,15 +405,15 @@
    1.14          val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
    1.15          fun needed c = valOf (Symtab.lookup ct c) > 0
    1.16          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
    1.17 -                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
    1.18 +                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
    1.19                   else []
    1.20          val BC = if needed "c_COMBB" orelse needed "c_COMBC"
    1.21 -                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
    1.22 +                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
    1.23                   else []
    1.24          val S = if needed "c_COMBS"
    1.25 -                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
    1.26 +                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
    1.27                  else []
    1.28 -        val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
    1.29 +        val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
    1.30      in
    1.31          map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
    1.32      end;