# HG changeset patch
# User fleury
# Date 1406721838 -7200
# Node ID 4546c9fdd8a701f5c8d8b40becbde3a5d39d0eaf
# Parent  cf8e4b1acd33eb8e81473aee8f5b75083f832c30
Improving robustness and indentation corrections.

diff -r cf8e4b1acd33 -r 4546c9fdd8a7 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:58 2014 +0200
@@ -99,8 +99,8 @@
     (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
       'c) ATP_Problem.atp_formula
     * string * (string * 'd list) list) list * string list
-  val core_inference :   'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
-      ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
+  val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
+    ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
   val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
   val core_of_agsyhol_proof :  string -> string list option
 end;
diff -r cf8e4b1acd33 -r 4546c9fdd8a7 src/HOL/Tools/ATP/atp_satallax.ML
--- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:58 2014 +0200
@@ -30,7 +30,7 @@
   ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id))
   -- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",")
   -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id
-         -- Scan.repeat ($$ "," |-- scan_general_id)) >> (op ::)) --| $$ "]"))
+         -- Scan.repeat ($$ "," |-- scan_general_id)) >> op ::) --| $$ "]"))
          || (skip_term >> K "") >> (fn x => SOME [x]))
        >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
 
@@ -39,12 +39,12 @@
 
 fun parse_prems x =
   (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]")
-     >> (op ::)) x
+     >> op ::) x
 
 fun parse_tstp_satallax_extra_arguments x =
   ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," )
   -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information
-  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> (op ::))
+  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> op ::)
   --| $$ "]") --
   (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) []
     >> (fn (x, []) => x | (_, x) => x))
diff -r cf8e4b1acd33 -r 4546c9fdd8a7 src/HOL/Tools/SMT2/verit_proof.ML
--- 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:58 2014 +0200
@@ -63,7 +63,7 @@
 fun node_of p cx =
   ([], cx)
   ||>> with_fresh_names (term_of p)
-  |>> (fn (_, (t, ns)) => (t, ns))
+  |>> snd
 
 (*in order to get Z3-style quantification*)
 fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) =
@@ -87,14 +87,6 @@
      replace_bound_var_by_free_var v free_vars
   | replace_bound_var_by_free_var u _ = u
 
-fun replace_bound_all_by_ex ((q as Const (_, typ)) $ Abs (var, ty, u)) free_var =
-    (case List.find (fn v => String.isPrefix v var) free_var of
-      NONE => q $ Abs (var, ty, replace_bound_all_by_ex u free_var)
-    | SOME _ => Const (@{const_name "HOL.Ex"}, typ) $ Abs (var, ty, replace_bound_all_by_ex u free_var))
-  | replace_bound_all_by_ex (u $ v) free_vars = replace_bound_all_by_ex u free_vars $
-     replace_bound_all_by_ex v free_vars
-  | replace_bound_all_by_ex u _ = u
-
 fun find_type_in_formula (Abs(v, ty, u)) var_name =
     if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name
   | find_type_in_formula (u $ v) var_name =
@@ -129,7 +121,7 @@
     fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl,
         bounds}) =
       if List.find (curry (op =) assumption_id) prems <> NONE then
-        let 
+        let
           val prems' = filter_out (curry (op =) assumption_id) prems
         in
           mk_node id rule (filter_out (curry (op =) assumption_id) prems')
@@ -139,16 +131,16 @@
       else
         st
     fun find_input_steps_and_inline [] last_step = ([], last_step)
-      | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) 
+      | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
           last_step =
         if rule = veriT_input_rule then
           find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step
         else
           apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds))
             (find_input_steps_and_inline steps (id_of_father_step ^ id'))
-    val (subproof', last_step_id) = find_input_steps_and_inline subproof "~1"
+    val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
     val prems' =
-      if last_step_id = "~1" then prems
+      if last_step_id = "" then prems
       else
         (case prems of
           NONE => SOME [last_step_id]
@@ -205,7 +197,7 @@
     #> fix_subproof_steps
     ##> to_node
     #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
-    #> uncurry (fold_map update_step_and_cx)
+    #-> (fold_map update_step_and_cx)
   end
 
 
@@ -293,10 +285,12 @@
       (*if the introduced var has already been defined,
         adding the definition as a dependency*)
       let
-        val SOME var = find_ite_var_in_term concl
-        val new_dep = find_in_which_step_defined var steps
+        val new_prems =
+          (case find_ite_var_in_term concl of
+            NONE => prems
+          | SOME var => find_in_which_step_defined var steps :: prems)
       in
-        VeriT_Node {id = id, rule = rule, prems = new_dep :: prems, concl = concl, bounds = bounds}
+        VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
       end
     else
       (*some new variables are created*)
diff -r cf8e4b1acd33 -r 4546c9fdd8a7 src/HOL/Tools/SMT2/verit_proof_parse.ML
--- 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:58 2014 +0200
@@ -68,8 +68,8 @@
 
 fun add_missing_steps iidths =
   let
-    fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id, rule = "input",
-      prems = [], concl = prop_of th, fixes = []}
+    fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id,
+      rule = veriT_input_rule, prems = [], concl = prop_of th, fixes = []}
   in map add_single_step iidths end
 
 fun parse_proof _