--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Aug 19 19:34:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 20 10:58:01 2010 +0200
@@ -83,7 +83,7 @@
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_term" in "ATP_Systems".) *)
+ (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
fun extensionalize_theorem th =
case prop_of th of
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
@@ -223,12 +223,13 @@
(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
into NNF. *)
fun to_nnf th ctxt0 =
- let val th1 = th |> transform_elim_theorem |> zero_var_indexes
- val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize_theorem
- |> Meson.make_nnf ctxt
- in (th3, ctxt) end;
+ let
+ val th1 = th |> transform_elim_theorem |> zero_var_indexes
+ val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize_theorem
+ |> Meson.make_nnf ctxt
+ in (th3, ctxt) end
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
fun cnf_axiom thy th =