src/HOL/Tools/res_atp_setup.ML

     if is_fol then 
 	(case ResClause.make_axiom_clause tm (name,i) of 
              SOME cls => (FOLClause cls) :: cls_axiom true  name (i+1) tms
            | NONE => cls_axiom true name i tms)
     else
-	(HOLClause (ResHolClause.make_axiom_clause tm (name,i))) :: (cls_axiom false name (i+1) tms);
+	HOLClause (ResHolClause.make_axiom_clause tm (name,i)) :: 
+	cls_axiom false name (i+1) tms;
 
 
 fun filtered_tptp_axiom is_fol name clss =
-    (fst(ListPair.unzip (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))),[])
-    handle _ => ([],[name]);
+  (fst
+   (ListPair.unzip 
+    (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))),
+   [])   handle _ => ([],[name]);
 
 fun tptp_axioms_aux _ [] err = ([],err)
   | tptp_axioms_aux is_fol ((name,clss)::nclss) err =
     let val (nclss1,err1) = tptp_axioms_aux is_fol nclss err
 	val (clsstrs,err_name_list) = filtered_tptp_axiom is_fol name clss

 (******* write to files ******)
 
 datatype mode = Auto | Fol | Hol;
 
 fun write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
-    let val is_fol = is_fol_logic logic
-	val (files1,err1) = if (null claR) then ([],[]) else (atp_axioms is_fol claR (claset_file()))
-	val (files2,err2) = if (null simpR) then ([],[]) else (atp_axioms is_fol simpR (simpset_file ()))
-	val (files3,err3) = if (null userR) then ([],[]) else (atp_axioms is_fol userR (local_lemma_file ()))
-	val files4 = atp_conjectures is_fol hyp_cls conj_cls n
-	val errs = err1 @ err2 @ err3 @ err
-	val logic' = if !include_combS then HOLCS 
-		     else 
-			 if !include_min_comb then HOLC else logic
-	val _ = warning ("Problems are " ^ (string_of_logic logic'))
-	val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
-	val helpers = case logic' of FOL => []
-				   | HOL => [HOL_helper1 ()]
-				   | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
-    in
-	(helpers,files4 @ files1 @ files2 @ files3)
-    end;
+  let val is_fol = is_fol_logic logic
+      val (files1,err1) = if (null claR) then ([],[]) 
+                          else (atp_axioms is_fol claR (claset_file()))
+      val (files2,err2) = if (null simpR) then ([],[]) 
+                          else (atp_axioms is_fol simpR (simpset_file ()))
+      val (files3,err3) = if (null userR) then ([],[]) 
+                          else (atp_axioms is_fol userR (local_lemma_file ()))
+      val files4 = atp_conjectures is_fol hyp_cls conj_cls n
+      val errs = err1 @ err2 @ err3 @ err
+      val logic' = if !include_combS then HOLCS 
+		   else 
+		       if !include_min_comb then HOLC else logic
+      val _ = warning ("Problems are " ^ (string_of_logic logic'))
+      val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
+      val helpers = case logic' of FOL => []
+				 | HOL => [HOL_helper1 ()]
+				 | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
+  in
+      (helpers,files4 @ files1 @ files2 @ files3)
+  end;
 
 
 fun write_out_ts is_fol ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
     let val ts_file = if ((is_fol andalso (!fol_keep_types)) orelse ((not is_fol) andalso (is_typed_hol ()))) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
 	val logic = if is_fol then FOL else HOL

     end;
  
 
 fun prep_atp_input mode ctxt conjectures user_thms n =
     let val conj_cls = map prop_of (make_clauses conjectures) 
-	val (userR,simpR,claR,errs) = cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset) 
+	val (userR,simpR,claR,errs) = 
+	    cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset) 
 	val hyp_cls = map prop_of (cnf_hyps_thms ctxt) 
 	val logic = case mode of Auto => problem_logic (conj_cls,hyp_cls,userR,claR,simpR)
 			       | Fol => FOL
 			       | Hol => HOL
     in