adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
authorblanchet
Mon Jun 14 10:36:01 2010 +0200 (2010-06-14)
changeset 374102bf7e6136047
parent 37409 6c9f23863808
child 37412 8cd75d103af9
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Sat Jun 12 15:48:17 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Jun 14 10:36:01 2010 +0200
     1.3 @@ -25,11 +25,8 @@
     1.4    ("Tools/Sledgehammer/metis_tactics.ML")
     1.5  begin
     1.6  
     1.7 -definition skolem_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
     1.8 -[no_atp]: "skolem_Eps = Eps"
     1.9 -
    1.10 -lemma skolem_someI_ex [no_atp]: "\<exists>x. P x \<Longrightarrow> P (skolem_Eps (\<lambda>x. P x))"
    1.11 -unfolding skolem_Eps_def by (rule someI_ex)
    1.12 +definition skolem_id :: "'a \<Rightarrow> 'a" where
    1.13 +[no_atp]: "skolem_id = (\<lambda>x. x)"
    1.14  
    1.15  definition COMBI :: "'a \<Rightarrow> 'a" where
    1.16  [no_atp]: "COMBI P \<equiv> P"
     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Jun 12 15:48:17 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 14 10:36:01 2010 +0200
     2.3 @@ -139,7 +139,7 @@
     2.4    let
     2.5      val thy = ProofContext.theory_of ctxt
     2.6      val (skolem_somes, (mlits, types_sorts)) =
     2.7 -     th |> prop_of |> kill_skolem_Eps j skolem_somes
     2.8 +     th |> prop_of |> conceal_skolem_somes j skolem_somes
     2.9          ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
    2.10    in
    2.11        if is_conjecture then
    2.12 @@ -235,24 +235,14 @@
    2.13            SOME tf => mk_tfree ctxt tf
    2.14          | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
    2.15  
    2.16 -fun reintroduce_skolem_Eps thy skolem_somes =
    2.17 -  let
    2.18 -    fun aux Ts args t =
    2.19 -      case t of
    2.20 -        t1 $ t2 => aux Ts (aux Ts [] t2 :: args) t1
    2.21 -      | Abs (s, T, t') => list_comb (Abs (s, T, aux (T :: Ts) [] t'), args)
    2.22 -      | Const (s, T) =>
    2.23 -        if String.isPrefix skolem_Eps_pseudo_theory s then
    2.24 -          let
    2.25 -            val (T', args', def') = AList.lookup (op =) skolem_somes s |> the
    2.26 -          in
    2.27 -            def' |> subst_free (args' ~~ args)
    2.28 -                 |> map_types Type_Infer.paramify_vars
    2.29 -          end
    2.30 -        else
    2.31 -          list_comb (t, args)
    2.32 -      | t => list_comb (t, args)
    2.33 -  in aux [] [] end
    2.34 +fun reveal_skolem_somes skolem_somes =
    2.35 +  map_aterms (fn t as Const (s, T) =>
    2.36 +                 if String.isPrefix skolem_theory_name s then
    2.37 +                   AList.lookup (op =) skolem_somes s
    2.38 +                   |> the |> map_types Type_Infer.paramify_vars
    2.39 +                 else
    2.40 +                   t
    2.41 +               | t => t)
    2.42  
    2.43  (*Maps metis terms to isabelle terms*)
    2.44  fun hol_term_from_fol_PT ctxt fol_tm =
    2.45 @@ -360,8 +350,7 @@
    2.46        val ts = map (hol_term_from_fol mode ctxt) fol_tms
    2.47        val _ = trace_msg (fn () => "  calling type inference:")
    2.48        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
    2.49 -      val ts' =
    2.50 -        ts |> map (reintroduce_skolem_Eps thy skolem_somes) |> infer_types ctxt
    2.51 +      val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
    2.52        val _ = app (fn t => trace_msg
    2.53                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    2.54                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
    2.55 @@ -418,7 +407,7 @@
    2.56        fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
    2.57        fun subst_translation (x,y) =
    2.58              let val v = find_var x
    2.59 -                (* We call "reintroduce_skolem_Eps" and "infer_types" below. *)
    2.60 +                (* We call "reveal_skolem_somes" and "infer_types" below. *)
    2.61                  val t = hol_term_from_fol mode ctxt y
    2.62              in  SOME (cterm_of thy (Var v), t)  end
    2.63              handle Option =>
    2.64 @@ -434,7 +423,7 @@
    2.65        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    2.66        val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
    2.67        val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
    2.68 -      val tms = rawtms |> map (reintroduce_skolem_Eps thy skolem_somes)
    2.69 +      val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
    2.70                         |> infer_types ctxt
    2.71        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
    2.72        val substs' = ListPair.zip (vars, map ctm_of tms)
    2.73 @@ -638,7 +627,7 @@
    2.74  type logic_map =
    2.75    {axioms: (Metis.Thm.thm * thm) list,
    2.76     tfrees: type_literal list,
    2.77 -   skolem_somes: (string * (typ * term list * term)) list}
    2.78 +   skolem_somes: (string * term) list}
    2.79  
    2.80  fun const_in_metis c (pred, tm_list) =
    2.81    let
    2.82 @@ -708,12 +697,7 @@
    2.83        val lmap =
    2.84          lmap |> mode <> FO
    2.85                  ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
    2.86 -  in
    2.87 -      (mode, add_type_thm (type_ext thy 
    2.88 -                                (* FIXME: Call"kill_skolem_Eps" here? *)
    2.89 -                          (map ((*snd o kill_skolem_Eps ~1 skolem_somes o*) prop_of)
    2.90 -                               (cls @ ths))) lmap)
    2.91 -  end;
    2.92 +  in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
    2.93  
    2.94  fun refute cls =
    2.95      Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Jun 12 15:48:17 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 14 10:36:01 2010 +0200
     3.3 @@ -117,7 +117,7 @@
     3.4        add_const_typ_table (const_with_typ thy (c,typ), tab) 
     3.5    | add_term_consts_typs_rm thy (Free(c, typ), tab) =
     3.6        add_const_typ_table (const_with_typ thy (c,typ), tab) 
     3.7 -  | add_term_consts_typs_rm _ (Const (@{const_name skolem_Eps}, _) $ _, tab) =
     3.8 +  | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) =
     3.9        tab
    3.10    | add_term_consts_typs_rm thy (t $ u, tab) =
    3.11        add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
    3.12 @@ -471,7 +471,8 @@
    3.13  (* ATP invocation methods setup                                *)
    3.14  (***************************************************************)
    3.15  
    3.16 -fun is_quasi_fol_term thy = Meson.is_fol_term thy o snd o kill_skolem_Eps ~1 []
    3.17 +fun is_quasi_fol_term thy =
    3.18 +  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 []
    3.19  
    3.20  (*Ensures that no higher-order theorems "leak out"*)
    3.21  fun restrict_to_logic thy true cls =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 12 15:48:17 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 14 10:36:01 2010 +0200
     4.3 @@ -10,11 +10,10 @@
     4.4    val chained_prefix: string
     4.5    val trace: bool Unsynchronized.ref
     4.6    val trace_msg: (unit -> string) -> unit
     4.7 -  val skolem_Eps_pseudo_theory: string
     4.8 +  val skolem_theory_name: string
     4.9    val skolem_prefix: string
    4.10    val skolem_infix: string
    4.11    val is_skolem_const_name: string -> bool
    4.12 -  val skolem_type_and_args: typ -> term -> typ * term list
    4.13    val cnf_axiom: theory -> thm -> thm list
    4.14    val multi_base_blacklist: string list
    4.15    val is_theorem_bad_for_atps: thm -> bool
    4.16 @@ -42,7 +41,7 @@
    4.17  val trace = Unsynchronized.ref false;
    4.18  fun trace_msg msg = if !trace then tracing (msg ()) else ();
    4.19  
    4.20 -val skolem_Eps_pseudo_theory = "Sledgehammer.Eps"
    4.21 +val skolem_theory_name = "Sledgehammer.Sko"
    4.22  val skolem_prefix = "sko_"
    4.23  val skolem_infix = "$"
    4.24  
    4.25 @@ -76,9 +75,6 @@
    4.26  
    4.27  (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    4.28  
    4.29 -fun skolem_Eps_const T =
    4.30 -  Const (@{const_name skolem_Eps}, (T --> HOLogic.boolT) --> T)
    4.31 -
    4.32  (*Keep the full complexity of the original name*)
    4.33  fun flatten_name s = space_implode "_X" (Long_Name.explode s);
    4.34  
    4.35 @@ -120,7 +116,7 @@
    4.36            val id = skolem_name s (Unsynchronized.inc skolem_count) s'
    4.37            val (cT, args) = skolem_type_and_args T body
    4.38            val rhs = list_abs_free (map dest_Free args,
    4.39 -                                   skolem_Eps_const T $ body)
    4.40 +                                   HOLogic.choice_const T $ body)
    4.41                    (*Forms a lambda-abstraction over the formal parameters*)
    4.42            val (c, thy) =
    4.43              Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
    4.44 @@ -139,6 +135,9 @@
    4.45        | dec_sko t thx = thx
    4.46    in dec_sko (prop_of th) ([], thy) end
    4.47  
    4.48 +fun mk_skolem_id t =
    4.49 +  let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) $ t end
    4.50 +
    4.51  (*Traverse a theorem, accumulating Skolem function definitions.*)
    4.52  fun assume_skolem_funs inline s th =
    4.53    let
    4.54 @@ -152,7 +151,9 @@
    4.55            val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
    4.56            val id = skolem_name s (Unsynchronized.inc skolem_count) s'
    4.57            val c = Free (id, cT)
    4.58 -          val rhs = list_abs_free (map dest_Free args, skolem_Eps_const T $ body)
    4.59 +          val rhs = list_abs_free (map dest_Free args,
    4.60 +                                   HOLogic.choice_const T $ body)
    4.61 +                    |> inline ? mk_skolem_id
    4.62                  (*Forms a lambda-abstraction over the formal parameters*)
    4.63            val def = Logic.mk_equals (c, rhs)
    4.64            val comb = list_comb (if inline then rhs else c, args)
    4.65 @@ -295,23 +296,26 @@
    4.66     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
    4.67  fun skolem_theorem_of_def inline def =
    4.68    let
    4.69 -      val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
    4.70 -      val (ch, frees) = c_variant_abs_multi (rhs, [])
    4.71 -      val (chilbert,cabs) = Thm.dest_comb ch
    4.72 +      val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
    4.73 +      val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
    4.74 +      val (ch, frees) = c_variant_abs_multi (rhs', [])
    4.75 +      val (chilbert, cabs) = ch |> Thm.dest_comb
    4.76        val thy = Thm.theory_of_cterm chilbert
    4.77        val t = Thm.term_of chilbert
    4.78        val T =
    4.79          case t of
    4.80 -          Const (@{const_name skolem_Eps}, Type (@{type_name fun}, [_, T])) => T
    4.81 -        | _ => raise THM ("skolem_theorem_of_def: expected \"Eps\"", 0, [def])
    4.82 +          Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
    4.83 +        | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
    4.84        val cex = Thm.cterm_of thy (HOLogic.exists_const T)
    4.85        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
    4.86        and conc =
    4.87          Drule.list_comb (if inline then rhs else c, frees)
    4.88          |> Drule.beta_conv cabs |> c_mkTrueprop
    4.89        fun tacf [prem] =
    4.90 -        (if inline then all_tac else rewrite_goals_tac [def])
    4.91 -        THEN rtac (prem RS @{thm skolem_someI_ex}) 1
    4.92 +        (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
    4.93 +         else rewrite_goals_tac [def])
    4.94 +        THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
    4.95 +                   RS @{thm someI_ex}) 1
    4.96    in  Goal.prove_internal [ex_tm] conc tacf
    4.97         |> forall_intr_list frees
    4.98         |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
    4.99 @@ -398,12 +402,7 @@
   4.100      let
   4.101        val ctxt0 = Variable.global_thm_context th
   4.102        val (nnfth, ctxt) = to_nnf th ctxt0
   4.103 -
   4.104 -      val inline = false
   4.105 -(*
   4.106 -FIXME: Reintroduce code:
   4.107        val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
   4.108 -*)
   4.109        val defs = skolem_theorems_of_assume inline s nnfth
   4.110        val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
   4.111      in
   4.112 @@ -492,7 +491,8 @@
   4.113          I
   4.114        else
   4.115          fold_index (fn (i, th) =>
   4.116 -          if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
   4.117 +          if is_theorem_bad_for_atps th orelse
   4.118 +             is_some (lookup_cache thy th) then
   4.119              I
   4.120            else
   4.121              cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Sat Jun 12 15:48:17 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 14 10:36:01 2010 +0200
     5.3 @@ -29,9 +29,8 @@
     5.4    val type_of_combterm : combterm -> fol_type
     5.5    val strip_combterm_comb : combterm -> combterm * combterm list
     5.6    val literals_of_term : theory -> term -> literal list * typ list
     5.7 -  val kill_skolem_Eps :
     5.8 -    int -> (string * (typ * term list * term)) list -> term
     5.9 -    -> (string * (typ * term list * term)) list * term
    5.10 +  val conceal_skolem_somes :
    5.11 +    int -> (string * term) list -> term -> (string * term) list * term
    5.12    exception TRIVIAL
    5.13    val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
    5.14    val make_axiom_clauses : bool -> theory ->
    5.15 @@ -123,7 +122,7 @@
    5.16        let
    5.17          val (tp, ts) = type_of dfg T
    5.18          val tvar_list =
    5.19 -          (if String.isPrefix skolem_Eps_pseudo_theory c then
    5.20 +          (if String.isPrefix skolem_theory_name c then
    5.21               [] |> Term.add_tvarsT T |> map TVar
    5.22             else
    5.23               (c, T) |> Sign.const_typargs thy)
    5.24 @@ -163,46 +162,24 @@
    5.25    skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
    5.26    skolem_infix ^ "g"
    5.27  
    5.28 -val flip_type =
    5.29 -  map_atyps (fn TFree (s, S) => TVar ((s, 0), S)
    5.30 -              | TVar ((s, 0), S) => TFree (s, S)
    5.31 -              | T as TVar (_, S) => raise TYPE ("nonzero TVar", [T], [])
    5.32 -              | T => T)
    5.33 -val flip_term =
    5.34 -  map_aterms (fn Free (s, T) => Var ((s, 0), T)
    5.35 -               | Var ((s, 0), T) => Free (s, T)
    5.36 -               | t as Var (_, S) => raise TERM ("nonzero Var", [t])
    5.37 -               | t => t)
    5.38 -  #> map_types flip_type
    5.39 -
    5.40 -fun flipped_skolem_type_and_args bound_T body =
    5.41 -  skolem_type_and_args (flip_type bound_T) (flip_term body)
    5.42 -  |>> flip_type ||> map flip_term
    5.43 -
    5.44 -fun triple_aconv ((T1, ts1, t1), (T2, ts2, t2)) =
    5.45 -  T1 = T2 andalso length ts1 = length ts2 andalso
    5.46 -  forall (op aconv) (ts1 ~~ ts2) andalso t1 aconv t2
    5.47 -
    5.48 -fun kill_skolem_Eps i skolem_somes t =
    5.49 -  if exists_Const (curry (op =) @{const_name skolem_Eps} o fst) t then
    5.50 +fun conceal_skolem_somes i skolem_somes t =
    5.51 +  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
    5.52      let
    5.53        fun aux skolem_somes
    5.54 -              (t as (Const (@{const_name skolem_Eps}, eps_T) $ t2)) =
    5.55 +              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
    5.56            let
    5.57 -            val bound_T = range_type eps_T
    5.58 -            val (T, args) = flipped_skolem_type_and_args bound_T t2
    5.59              val (skolem_somes, s) =
    5.60                if i = ~1 then
    5.61                  (skolem_somes, @{const_name undefined})
    5.62 -              else case AList.find triple_aconv skolem_somes (T, args, t) of
    5.63 +              else case AList.find (op aconv) skolem_somes t of
    5.64                  s :: _ => (skolem_somes, s)
    5.65                | _ =>
    5.66                  let
    5.67 -                  val s = skolem_Eps_pseudo_theory ^ "." ^
    5.68 +                  val s = skolem_theory_name ^ "." ^
    5.69                            skolem_name i (length skolem_somes)
    5.70                                          (length (Term.add_tvarsT T []))
    5.71 -                in ((s, (T, args, t)) :: skolem_somes, s) end
    5.72 -          in (skolem_somes, list_comb (Const (s, T), args)) end
    5.73 +                in ((s, t) :: skolem_somes, s) end
    5.74 +          in (skolem_somes, Const (s, T)) end
    5.75          | aux skolem_somes (t1 $ t2) =
    5.76            let
    5.77              val (skolem_somes, t1) = aux skolem_somes t1
    5.78 @@ -224,7 +201,7 @@
    5.79  fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
    5.80    let
    5.81      val (skolem_somes, t) =
    5.82 -      th |> prop_of |> kill_skolem_Eps clause_id skolem_somes
    5.83 +      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
    5.84      val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
    5.85    in
    5.86      if forall isFalse lits then
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sat Jun 12 15:48:17 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jun 14 10:36:01 2010 +0200
     6.3 @@ -261,8 +261,8 @@
     6.4     (instances of) Skolem pseudoconstants, this information is encoded in the
     6.5     constant name. *)
     6.6  fun num_type_args thy s =
     6.7 -  if String.isPrefix skolem_Eps_pseudo_theory s then
     6.8 -    s |> unprefix skolem_Eps_pseudo_theory
     6.9 +  if String.isPrefix skolem_theory_name s then
    6.10 +    s |> unprefix skolem_theory_name
    6.11        |> space_explode skolem_infix |> hd
    6.12        |> space_explode "_" |> List.last |> Int.fromString |> the
    6.13    else
    6.14 @@ -324,7 +324,7 @@
    6.15                          else
    6.16                            (* Extra args from "hAPP" come after any arguments
    6.17                               given directly to the constant. *)
    6.18 -                          if String.isPrefix skolem_Eps_pseudo_theory c then
    6.19 +                          if String.isPrefix skolem_theory_name c then
    6.20                              map fastype_of ts ---> HOLogic.typeT
    6.21                            else
    6.22                              Sign.const_instance thy (c,
     7.1 --- a/src/HOL/Tools/meson.ML	Sat Jun 12 15:48:17 2010 +0200
     7.2 +++ b/src/HOL/Tools/meson.ML	Mon Jun 14 10:36:01 2010 +0200
     7.3 @@ -98,9 +98,8 @@
     7.4            val tmA = concl_of thA
     7.5            val Const("==>",_) $ tmB $ _ = prop_of thB
     7.6            val tenv =
     7.7 -            Pattern.first_order_match thy
     7.8 -                (pairself Envir.beta_eta_contract (tmB, tmA))
     7.9 -                (Vartab.empty, Vartab.empty) |> snd
    7.10 +            Pattern.first_order_match thy (tmB, tmA)
    7.11 +                                          (Vartab.empty, Vartab.empty) |> snd
    7.12            val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    7.13        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    7.14      SOME th => th
    7.15 @@ -317,17 +316,17 @@
    7.16  val has_meta_conn =
    7.17      exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
    7.18  
    7.19 -fun apply_skolem_ths (th, rls) =
    7.20 +fun apply_skolem_theorem (th, rls) =
    7.21    let
    7.22 -    fun tryall [] = raise THM ("apply_skolem_ths", 0, th::rls)
    7.23 +    fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
    7.24        | tryall (rl :: rls) =
    7.25          first_order_resolve th rl handle THM _ => tryall rls
    7.26    in tryall rls end
    7.27  
    7.28 -(*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    7.29 -  Strips universal quantifiers and breaks up conjunctions.
    7.30 -  Eliminates existential quantifiers using skoths: Skolemization theorems.*)
    7.31 -fun cnf skoths ctxt (th,ths) =
    7.32 +(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    7.33 +   Strips universal quantifiers and breaks up conjunctions.
    7.34 +   Eliminates existential quantifiers using Skolemization theorems. *)
    7.35 +fun cnf skolem_ths ctxt (th, ths) =
    7.36    let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
    7.37        fun cnf_aux (th,ths) =
    7.38          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
    7.39 @@ -341,7 +340,7 @@
    7.40                  in  ctxtr := ctxt'; cnf_aux (th', ths) end
    7.41            | Const ("Ex", _) =>
    7.42                (*existential quantifier: Insert Skolem functions*)
    7.43 -              cnf_aux (apply_skolem_ths (th,skoths), ths)
    7.44 +              cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
    7.45            | Const ("op |", _) =>
    7.46                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    7.47                  all combinations of converting P, Q to CNF.*)
    7.48 @@ -357,7 +356,7 @@
    7.49              else cnf_aux (th,ths)
    7.50    in  (cls, !ctxtr)  end;
    7.51  
    7.52 -fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
    7.53 +fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []);
    7.54  
    7.55  (*Generalization, removal of redundant equalities, removal of tautologies.*)
    7.56  fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);