# HG changeset patch
# User fleury
# Date 1406721793 -7200
# Node ID 323a57d7455ce222a01365d5cbdffa69f5d4c187
# Parent  9cda0c64c37aa9fe1e229056a966e1454c1740c3
imported patch satallax_skolemization_in_tree_part

diff -r 9cda0c64c37a -r 323a57d7455c src/HOL/Tools/ATP/atp_satallax.ML
--- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -30,8 +30,9 @@
   ((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)) >> uncurry cons) --| $$ "]"))
-        || skip_term >> K NONE) >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
+         -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]"))
+         || (skip_term >> K "") >> (fn x => SOME [x]))
+       >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
 
 fun parse_prem x =
   ((Symbol.scan_ascii_id || scan_general_id) --| Scan.option ($$ ":" -- skip_term)) x
@@ -66,50 +67,57 @@
   assumptions: string list,
   rule: string,
   used_assumptions: string list,
+  detailed_eigen: string,
   generated_goal_assumptions: (string * string list) list}
 
 fun mk_satallax_step id role theorem assumptions rule used_assumptions
-      generated_goal_assumptions =
-    Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule,
-      used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions}
+    generated_goal_assumptions detailed_eigen =
+  Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule,
+    used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions,
+    detailed_eigen = detailed_eigen}
 
 fun get_assumptions (("assumptions", SOME (_ , assumptions)) :: _) =
     the_default [] assumptions
   | get_assumptions (_ :: l) = get_assumptions l
   | get_assumptions [] = []
 
+fun get_detailled_eigen ((_, SOME (SOME "eigenvar" , var)) :: _) =
+    hd (the_default [""] var)
+  | get_detailled_eigen (_ :: l) = get_detailled_eigen l
+  | get_detailled_eigen [] = ""
+
 fun seperate_dependices dependencies =
-    let
-      fun sep_dep [] used_assumptions new_goals generated_assumptions _ =
-          (used_assumptions, new_goals, generated_assumptions)
-        | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state =
-          if hd (raw_explode x) = "h" orelse Int.fromString x = NONE  then
-            if state = 0 then
-              sep_dep l (x :: used_assumptions) new_goals generated_assumptions state
-            else
-              sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3
+  let
+    fun sep_dep [] used_assumptions new_goals generated_assumptions _ =
+        (used_assumptions, new_goals, generated_assumptions)
+      | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state =
+        if hd (raw_explode x) = "h" orelse Int.fromString x = NONE  then
+          if state = 0 then
+            sep_dep l (x :: used_assumptions) new_goals generated_assumptions state
           else
-            if state = 1 orelse state = 0 then
-              sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1
-            else
-              raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l)
-    in
-      sep_dep dependencies [] [] [] 0
-    end
+            sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3
+        else
+          if state = 1 orelse state = 0 then
+            sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1
+          else
+            raise Fail ("incorrect Satallax proof" ^ PolyML.makestring l)
+  in
+    sep_dep dependencies [] [] [] 0
+  end
 
 fun create_grouped_goal_assumption rule new_goals generated_assumptions =
-    if length new_goals = length generated_assumptions then
-      new_goals ~~ (map single generated_assumptions)
-    else if 2 * length new_goals = length generated_assumptions then
-      let
-        fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
-            (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
-          | group_by_pair [] [] = []
-      in
-        group_by_pair new_goals generated_assumptions
-      end
-    else
-      raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
+  if length new_goals = length generated_assumptions then
+    new_goals ~~ (map single generated_assumptions)
+  else if 2 * length new_goals = length generated_assumptions then
+    let
+      fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
+          (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
+        | group_by_pair [] [] = []
+    in
+      group_by_pair new_goals generated_assumptions
+    end
+  else
+    raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
 
 fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
     let
@@ -117,32 +125,34 @@
     in
       mk_satallax_step id role formula (get_assumptions (the_default [] l)) rule used_assumptions
         (create_grouped_goal_assumption rule new_goals generated_assumptions)
+        (get_detailled_eigen (the_default [] l))
     end
   | to_satallax_step (((id, role), formula), NONE) =
-    mk_satallax_step id role formula [] "assumption" [] []
+      mk_satallax_step id role formula [] "assumption" [] [] ""
 
 fun is_assumption (Satallax_Step {role, ...}) = role = "assumption" orelse role = "axiom" orelse
   role = "negated_conjecture" orelse role = "conjecture"
 
 fun seperate_assumptions_and_steps l =
-    let
-      fun seperate_assumption [] l l' = (l, l')
-        | seperate_assumption (step :: steps) l l' =
-          if is_assumption step then
-            seperate_assumption steps (step :: l) l'
-          else
-            seperate_assumption steps l (step :: l')
-    in
-      seperate_assumption l [] []
-    end
+  let
+    fun seperate_assumption [] l l' = (l, l')
+      | seperate_assumption (step :: steps) l l' =
+        if is_assumption step then
+          seperate_assumption steps (step :: l) l'
+        else
+          seperate_assumption steps l (step :: l')
+  in
+    seperate_assumption l [] []
+  end
 
 datatype satallax_proof_graph =
-  Node_Source of {node: satallax_step, succs: satallax_proof_graph list} |
-  Node_Conclusion of {node: satallax_step, deps: satallax_proof_graph list}
+  Linear_Part of {node: satallax_step, succs: satallax_proof_graph list} |
+  Tree_Part of {node: satallax_step, deps: satallax_proof_graph list}
 
 fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h =
     if h = id then x else find_proof_step l h
-  | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h)
+  | find_proof_step [] h = raise Fail ("not_found: " ^ PolyML.makestring h ^ "(probably a parsing \
+    \error)")
 
 fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) =
     if op1 = op2 andalso op1 = tptp_not then th else x
@@ -152,6 +162,8 @@
     fold2 (fn t1 => fn t2 => fn c => c andalso t1 = t2) l1 l2 true
   | tptp_term_equal (_, _) = false
 
+val dummy_true_aterm = ATerm (("$true", [dummy_atype]), [])
+
 fun find_assumptions_to_inline ths (assm :: assms) to_inline no_inline =
     (case List.find (curry (op =) assm o fst) no_inline of
       SOME _ => find_assumptions_to_inline ths assms to_inline no_inline
@@ -171,109 +183,113 @@
 
 fun inline_if_needed_and_simplify th assms to_inline no_inline =
     (case find_assumptions_to_inline [th] assms to_inline no_inline of
-      [] => ATerm (("$true", [dummy_atype]), [])
-  | l => foldl1 (fn (a, b) => ATerm ((tptp_or, [dummy_atype]), [a, b])) l)
+      [] => dummy_true_aterm
+  | l => foldl1 (fn (a, b) =>
+    (case b of
+      ATerm (("$false", _), _) => a
+    | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a
+    | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l)
 
 
 fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem
 
-fun add_assumption new_used_assumptions  ((Satallax_Step {id, role, theorem, assumptions,
-      rule, generated_goal_assumptions, used_assumptions})) =
-    mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions)
-      generated_goal_assumptions
+fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions,
+    rule, generated_goal_assumptions, used_assumptions, detailed_eigen})) =
+  mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions)
+    generated_goal_assumptions detailed_eigen
 
 fun set_rule new_rule (Satallax_Step {id, role, theorem, assumptions,
-      generated_goal_assumptions, used_assumptions, ...}) =
-    mk_satallax_step id role theorem assumptions new_rule used_assumptions
-      generated_goal_assumptions
+    generated_goal_assumptions, used_assumptions, detailed_eigen, ...}) =
+  mk_satallax_step id role theorem assumptions new_rule used_assumptions
+    generated_goal_assumptions detailed_eigen
 
 fun transform_inline_assumption hypotheses_step proof_sketch =
   let
-    fun inline_in_step (Node_Source {node as Satallax_Step {generated_goal_assumptions,
-                                                            used_assumptions, rule, ...}, succs}) =
+    fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions,
+          used_assumptions, rule, ...}, succs}) =
         if generated_goal_assumptions = [] then
-            Node_Source {node = node, succs = []}
+            Linear_Part {node = node, succs = []}
         else
           let
             (*one singel goal is created, two hypothesis can be created, for the "and" rule:
               (A /\ B) create two hypotheses A, and B.*)
             fun set_hypotheses_as_goal [hypothesis] succs =
-                Node_Source {node = set_rule rule
-                    (add_assumption used_assumptions (find_proof_step hypotheses_step hypothesis)),
+                Linear_Part {node = set_rule rule (add_assumption used_assumptions 
+                    (find_proof_step hypotheses_step hypothesis)),
                   succs = map inline_in_step succs}
               | set_hypotheses_as_goal (hypothesis :: new_goal_hypotheses) succs =
-                Node_Source {node = set_rule rule
-                    (add_assumption used_assumptions (find_proof_step hypotheses_step hypothesis)),
+                Linear_Part {node = set_rule rule (add_assumption used_assumptions
+                    (find_proof_step hypotheses_step hypothesis)),
                   succs = [set_hypotheses_as_goal new_goal_hypotheses succs]}
           in
             set_hypotheses_as_goal (snd (hd generated_goal_assumptions)) succs
           end
-      | inline_in_step (Node_Conclusion {node = node, deps}) =
-        Node_Conclusion {node = node, deps = map inline_in_step deps}
+      | inline_in_step (Tree_Part {node = node, deps}) =
+        Tree_Part {node = node, deps = map inline_in_step deps}
 
-    fun inline_contradictory_assumptions (Node_Source {node as Satallax_Step{id, theorem, ...},
-           succs}) (to_inline, no_inline) =
-        let
-          val (succs, inliner) = fold_map inline_contradictory_assumptions
-                                          succs (to_inline, (id, theorem) :: no_inline)
-        in
-          (Node_Source {node = node, succs = succs}, inliner)
-        end
-      | inline_contradictory_assumptions (Node_Conclusion {node = Satallax_Step {id, role,
-          theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions,
-          used_assumptions}, deps}) (to_inline, no_inline) =
-        let
-          val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions
-                                                          deps (to_inline, no_inline)
-          val to_inline'' = map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s)))
-                                (List.filter (fn s => nth_string s 0 = "h")
-                                             (used_assumptions @
-                                               (map snd generated_goal_assumptions |> flat)))
-                            @ to_inline'
-          val node' = Satallax_Step {id = id, role = role, theorem =
-                AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'),
-              assumptions = assumptions, rule = rule,
-              generated_goal_assumptions = generated_goal_assumptions,
-              used_assumptions =
-                List.filter (fn s => List.find (curry (op =) s o fst) to_inline = NONE)
-                used_assumptions}
-        in
-          (Node_Conclusion {node = node', deps = dep'}, (to_inline'', no_inline'))
-        end
+    fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...},
+       succs}) (to_inline, no_inline) =
+      let
+        val (succs, inliner) = fold_map inline_contradictory_assumptions
+                                        succs (to_inline, (id, theorem) :: no_inline)
+      in
+        (Linear_Part {node = node, succs = succs}, inliner)
+      end
+    | inline_contradictory_assumptions (Tree_Part {node = Satallax_Step {id, role,
+        theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions,
+        used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) =
+      let
+        val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions
+                                                        deps (to_inline, no_inline)
+        val to_inline'' =
+          map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s)))
+            (List.filter (fn s => nth_string s 0 = "h")
+              (used_assumptions @ (map snd generated_goal_assumptions |> flat)))
+          @ to_inline'
+        val node' = Satallax_Step {id = id, role = role, theorem =
+            AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'),
+          assumptions = assumptions, rule = rule,
+          generated_goal_assumptions = generated_goal_assumptions, detailed_eigen = detailed_eigen,
+          used_assumptions =
+            List.filter (fn s => List.find (curry (op =) s o fst) to_inline = NONE)
+            used_assumptions}
+      in
+        (Tree_Part {node = node', deps = dep'}, (to_inline'', no_inline'))
+      end
   in
     fst (inline_contradictory_assumptions (inline_in_step proof_sketch) ([], []))
   end
 
-fun correct_dependencies (Node_Source {node, succs}) =
-    Node_Source {node = node, succs = map correct_dependencies succs}
-  | correct_dependencies (Node_Conclusion {node, deps}) =
+fun correct_dependencies (Linear_Part {node, succs}) =
+    Linear_Part {node = node, succs = map correct_dependencies succs}
+  | correct_dependencies (Tree_Part {node, deps}) =
     let
       val new_used_assumptions =
-          map (fn Node_Source {node = (Satallax_Step{id, ...}), ...} => id
-                | Node_Conclusion {node = (Satallax_Step{id, ...}), ...} => id) deps
+        map (fn Linear_Part {node = (Satallax_Step{id, ...}), ...} => id
+              | Tree_Part {node = (Satallax_Step{id, ...}), ...} => id) deps
     in
-      Node_Conclusion {node = add_assumption new_used_assumptions node,
+      Tree_Part {node = add_assumption new_used_assumptions node,
         deps = map correct_dependencies deps}
     end
 
 fun create_satallax_proof_graph (hypotheses_step, proof_sketch) =
-    let
-      fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) =
-        Node_Source {node = step,
-          succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch)))
-            (map fst generated_goal_assumptions)}
-      fun reverted_discharged_steps is_branched (Node_Source {node as
-            Satallax_Step {generated_goal_assumptions, ...}, succs}) =
-          if is_branched orelse length generated_goal_assumptions > 1 then
-            Node_Conclusion {node = node, deps = map (reverted_discharged_steps true) succs}
-          else
-            Node_Source {node = node, succs = map (reverted_discharged_steps is_branched) succs}
-      val proof_with_correct_sense =
-          correct_dependencies (reverted_discharged_steps false
-            (create_step (find_proof_step proof_sketch "0" )))
-    in
-      transform_inline_assumption hypotheses_step proof_with_correct_sense
-    end
+  let
+    fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) =
+      Linear_Part {node = step,
+        succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch)))
+          (map fst generated_goal_assumptions)}
+    fun reverted_discharged_steps is_branched (Linear_Part {node as
+          Satallax_Step {generated_goal_assumptions, ...}, succs}) =
+        if is_branched orelse length generated_goal_assumptions > 1 then
+          Tree_Part {node = node, deps = map (reverted_discharged_steps true) succs}
+        else
+          Linear_Part {node = node, succs = map (reverted_discharged_steps is_branched) succs}
+    val proof_with_correct_sense =
+        correct_dependencies (reverted_discharged_steps false
+          (create_step (find_proof_step proof_sketch "0" )))
+  in
+    transform_inline_assumption hypotheses_step proof_with_correct_sense
+  end
 
 val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true",
     "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq",
@@ -281,29 +297,85 @@
     "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"]
 val is_special_satallax_rule = member (op =) satallax_known_theorems
 
+fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) =
+     let
+       val bdy = terms_to_upper_case var b
+       val ts' = map (terms_to_upper_case var) ts
+     in
+      AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty),
+        bdy), ts')
+    end
+  | terms_to_upper_case var (ATerm ((var', ty), ts)) =
+    ATerm ((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'),
+      ty), map (terms_to_upper_case var) ts)
 
-fun transform_to_standard_atp_step proof =
+fun add_quantifier_in_tree_part vars_to_add assumption_to_add (Linear_Part {node, succs}) =
+    Linear_Part {node = node, succs = map (add_quantifier_in_tree_part vars_to_add assumption_to_add) succs}
+  | add_quantifier_in_tree_part vars_to_add assumption_to_add (Tree_Part {node = Satallax_Step {rule, detailed_eigen,
+      id, role, theorem = AAtom theorem, assumptions, used_assumptions, generated_goal_assumptions},
+      deps}) =
     let
-      fun create_fact_step id =
-        ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", [])
-      fun transform_one_step (Satallax_Step {id, theorem, used_assumptions, role, rule, ...}) =
-        let
-          val role' = role_of_tptp_string role
-        in
-          map create_fact_step
-            (List.filter (fn s => size s >=4 andalso not (is_special_satallax_rule s))
-            used_assumptions)
-          @ [((id, []), if role' = Unknown then Plain else role', theorem, rule,
-              map (fn s => (s, [])) used_assumptions)]
-        end
+      val theorem' = fold (fn v => fn body => terms_to_upper_case v body) vars_to_add theorem
+      val theorem'' = theorem'
+      val node' = mk_satallax_step id role (AAtom theorem'') assumptions rule
+        (used_assumptions @ (filter (curry (op <=) (the (Int.fromString id)) o size)
+        assumption_to_add)) generated_goal_assumptions detailed_eigen
+    in
+      if detailed_eigen <> "" then
+        Tree_Part {node = node',
+          deps = map (add_quantifier_in_tree_part (detailed_eigen :: vars_to_add)
+          (used_assumptions @ assumption_to_add)) deps}
+      else
+        Tree_Part {node = node',
+                   deps = map (add_quantifier_in_tree_part vars_to_add assumption_to_add) deps}
+    end
 
-      fun transform_steps (Node_Source {node, succs}) =
-          transform_one_step node @ (map transform_steps succs |> flat)
-        | transform_steps (Node_Conclusion {node, deps}) =
-          ((map transform_steps deps) |> flat) @ (transform_one_step node)
-    in
-      transform_steps proof
-    end
+fun transform_to_standard_atp_step already_transformed proof =
+  let
+    fun create_fact_step id =
+      ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", [])
+    fun transform_one_step already_transformed (Satallax_Step {id, theorem, used_assumptions, role,
+        rule, ...}) =
+      let
+        val role' = role_of_tptp_string role
+        val new_transformed = List.filter
+          (fn s => size s >=4 andalso not (is_special_satallax_rule s) andalso not
+          (member (op =) already_transformed s)) used_assumptions
+      in
+        (map create_fact_step new_transformed
+        @ [((id, []), if role' = Unknown then Plain else role', theorem, rule,
+           map (fn s => (s, [])) (filter_out is_special_satallax_rule used_assumptions))],
+        new_transformed @ already_transformed)
+      end
+    fun transform_steps (Linear_Part {node, succs}) (already_transformed:string list) =
+        transform_one_step already_transformed node
+        ||> (fold_map transform_steps succs)
+        ||> apfst flat
+        |> (fn (a, (b, transformed)) => (a @ b, transformed))
+      | transform_steps (Tree_Part {node, deps}) (already_transformed: string list) =
+        fold_map transform_steps deps already_transformed
+        |>> flat
+        ||> (fn transformed => transform_one_step transformed node)
+        |> (fn (a, (b, transformed)) => (a @ b, transformed))
+  in
+    fst (transform_steps proof already_transformed)
+  end
+
+fun remove_unused_dependency steps =
+  let
+    fun find_all_ids [] = []
+     | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps
+    fun keep_only_used used_ids steps =
+      let
+        fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) =
+            (((id, ids), role, theorem, rule, filter (member (op =) used_ids o fst) deps) :: steps)
+          | remove_unused [] = []
+      in
+        remove_unused steps
+      end
+  in
+    keep_only_used (find_all_ids steps) steps
+  end
 
 
 fun parse_proof local_name problem =
@@ -317,13 +389,14 @@
       else
         (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
           (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
-          #> fst
-          #> rev
-          #> map to_satallax_step
-          #> seperate_assumptions_and_steps
-          #> create_satallax_proof_graph
-          #> transform_to_standard_atp_step))
-
+            #> fst
+            #> rev
+            #> map to_satallax_step
+            #> seperate_assumptions_and_steps
+            #> create_satallax_proof_graph
+            #> add_quantifier_in_tree_part [] []
+            #> transform_to_standard_atp_step []
+            #> remove_unused_dependency))
 
 fun atp_proof_of_tstplike_proof _ _ "" = []
   | atp_proof_of_tstplike_proof local_prover problem tstp =
@@ -335,5 +408,4 @@
       |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
       |> local_prover = zipperpositionN ? rev)
 
-
 end;
diff -r 9cda0c64c37a -r 323a57d7455c src/HOL/Tools/SMT2/smtlib2_isar.ML
--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -47,11 +47,6 @@
     t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
   | _ => t)
 
-(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
-val unskolemize_names =
-  Term.map_abs_vars (perhaps (try Name.dest_skolem))
-  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
-
 fun unlift_term ll_defs =
   let
     val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
diff -r 9cda0c64c37a -r 323a57d7455c src/HOL/Tools/SMT2/verit_proof.ML
--- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -29,8 +29,6 @@
 
 open SMTLIB2_Proof
 
-(* proof rules *)
-
 datatype veriT_node = VeriT_Node of {
   id: int,
   rule: string,