--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200
@@ -345,9 +345,8 @@
|> filter is_zapped_var_name
val ctxt' = ctxt |> Variable.add_fixes_direct fixes
val fully_skolemized_t =
- zapped_th
- |> singleton (Variable.export ctxt' ctxt)
- |> cprop_of |> Thm.dest_equals |> snd |> term_of
+ zapped_th |> singleton (Variable.export ctxt' ctxt)
+ |> cprop_of |> Thm.dest_equals |> snd |> term_of
in
if exists_subterm (fn Var ((s, _), _) =>
String.isPrefix new_skolem_var_prefix s