--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri May 24 16:43:37 2013 +0200
@@ -799,8 +799,8 @@
fun lift_lams_part_2 ctxt (facts, lifted) =
(facts, lifted)
- (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
- of them *)
+ (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
+ get rid of them *)
|> pairself (map (introduce_combinators ctxt))
|> pairself (map constify_lifted)
(* Requires bound variables not to clash with any schematic variables (as