Whitespace and indentation correction.

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -239,13 +239,13 @@
           in
             if textual then
               (case ts of
-                [fst, lst] =>
-                if loose_aconv (fst, lst) then
+                [t1, t2] =>
+                if loose_aconv (t1, t2) then
                   @{const True}
-                else if Term.aconv_untyped (lst, @{const True}) then
-                  fst
-                else if Term.aconv_untyped (fst, @{const True}) then
-                  lst
+                else if Term.aconv_untyped (t2, @{const True}) then
+                  t1
+                else if Term.aconv_untyped (t1, @{const True}) then
+                  t2
                 else
                   equal_term ts
               | _ => equal_term ts)

--- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -39,7 +39,6 @@
 fun mk_node id rule prems concl bounds =
   VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
 
-(*two structures needed*)
 datatype veriT_step = VeriT_Step of {
   id: string,
   rule: string,
@@ -54,8 +53,8 @@
 val veriT_input_rule = "input"
 val veriT_rewrite_rule = "__rewrite" (*arbitrary*)
 val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
-val veriT_tmp_skolemize = "tmp_skolemize"
-val veriT_alpha_conv = "tmp_alphaconv"
+val veriT_tmp_skolemize_rule = "tmp_skolemize"
+val veriT_alpha_conv_rule = "tmp_alphaconv"
 
 (* proof parser *)
 
@@ -102,7 +101,7 @@
 fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx =
   if rule = veriT_tmp_ite_elim_rule then
     (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl)
-  else if rule = veriT_tmp_skolemize then
+  else if rule = veriT_tmp_skolemize_rule then
     let
       val concl' = replace_bound_var_by_free_var concl bounds
     in
@@ -159,7 +158,6 @@
     fun rotate_pair (a, (b, c)) = ((a, b), c)
     fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l)
       | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t)
-    fun unprefix_id x = (*unprefix veriT_step_prefix*) x
     fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l)
     fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) =
         (SOME (map (fn (SMTLIB2.Sym id) => id) source), l)
@@ -177,10 +175,9 @@
         (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
         perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
     fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule
-          (the_default [] prems) concl bounds, cx)
+      (the_default [] prems) concl bounds, cx)
   in
     get_id
-    #>> unprefix_id
     ##> parse_rule
     #> rotate_pair
     ##> parse_source
@@ -217,7 +214,7 @@
           if m + n = 0 then
             [actual_lines ^ line] :: seperate l "" 0
           else seperate l (actual_lines ^ line) (m + n)
-      end
+        end
       | seperate [] _ 0 = []
   in
     seperate lines "" 0
@@ -296,7 +293,7 @@
       let
         val concl' = replace_bound_var_by_free_var concl bounds
       in
-        mk_node id veriT_tmp_skolemize prems concl' []
+        mk_node id veriT_tmp_skolemize_rule prems concl' []
       end
   else
     st
@@ -309,7 +306,7 @@
         map (fn x => perhaps (Symtab.lookup replace_table) x) prems
       fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem
     in
-      if rule = veriT_alpha_conv then
+      if rule = veriT_alpha_conv_rule then
         remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
           replace_table) steps
       else

--- a/src/HOL/Tools/SMT2/verit_proof_parse.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -39,9 +39,9 @@
             NONE =>
             let
               val id' = if th = ll_offset then 0 else id - ll_offset (* 0: for the conjecture*)
-              val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths
-                                                          (if th <> ll_offset then id + 1 else id)
-                                                          ((x, string_of_int id') :: replaced)
+              val ((prems, iidths), (id'', replaced')) =
+                prems_to_theorem_number ths (if th <> ll_offset then id + 1 else id)
+                  ((x, string_of_int id') :: replaced)
             in
               ((string_of_int id' :: prems, (th, (id', th - ll_offset)) :: iidths),
                (id'', replaced'))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -61,9 +61,9 @@
 val zipperposition_cnf_rule = "cnf"
 
 val skolemize_rules =
-  [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
-zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule,
-satallax_skolemize_rule]
+  [e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule,
+    vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
+    zipperposition_cnf_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -258,7 +258,6 @@
 
 val canonical_isar_supported_prover = eN
 val z3N = "z3"
-val veriT_newN = "veriT"
 
 fun isar_supported_prover_of thy name =
   if is_atp thy name orelse name = z3N then name