1.1 --- a/src/HOL/Tools/meson.ML	Tue Jan 13 16:47:24 2009 +0000
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jan 29 12:05:19 2009 +0000
     1.3 @@ -15,7 +15,6 @@
     1.4    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     1.5    val finish_cnf: thm list -> thm list
     1.6    val make_nnf: thm -> thm
     1.7 -  val make_nnf1: thm -> thm
     1.8    val skolemize: thm -> thm
     1.9    val is_fol_term: theory -> term -> bool
    1.10    val make_clauses: thm list -> thm list
    1.11 @@ -296,7 +295,7 @@
    1.12  (*Any need to extend this list with
    1.13    "HOL.type_class","HOL.eq_class","Pure.term"?*)
    1.14  val has_meta_conn =
    1.15 -    exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
    1.16 +    exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
    1.17  
    1.18  fun apply_skolem_ths (th, rls) =
    1.19    let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
    1.20 @@ -519,19 +518,21 @@
    1.21  
    1.22  (*Pull existential quantifiers to front. This accomplishes Skolemization for
    1.23    clauses that arise from a subgoal.*)
    1.24 -fun skolemize th =
    1.25 +fun skolemize1 th =
    1.26    if not (has_conns ["Ex"] (prop_of th)) then th
    1.27 -  else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    1.28 +  else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2,
    1.29                                disj_exD, disj_exD1, disj_exD2])))
    1.30      handle THM ("tryres", _, _) =>
    1.31 -        skolemize (forward_res skolemize
    1.32 +        skolemize1 (forward_res skolemize1
    1.33                     (tryres (th, [conj_forward, disj_forward, all_forward])))
    1.34      handle THM ("tryres", _, _) => 
    1.35 -        forward_res skolemize (rename_bvs_RS th ex_forward);
    1.36 +        forward_res skolemize1 (rename_bvs_RS th ex_forward);
    1.37 +
    1.38 +fun skolemize th = skolemize1 (make_nnf th);
    1.39  
    1.40  fun skolemize_nnf_list [] = []
    1.41    | skolemize_nnf_list (th::ths) = 
    1.42 -      skolemize (make_nnf th) :: skolemize_nnf_list ths
    1.43 +      skolemize th :: skolemize_nnf_list ths
    1.44        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
    1.45         (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
    1.46          skolemize_nnf_list ths);