# HG changeset patch
# User blanchet
# Date 1391096431 -3600
# Node ID a0bd8d6414e69ab8ef44a9d2d358caa89f1f92c7
# Parent  6e2295db4cf8edae59c5e02849e8b92ea0a0475e
centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)

diff -r 6e2295db4cf8 -r a0bd8d6414e6 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 30 15:01:40 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 30 16:40:31 2014 +0100
@@ -155,7 +155,7 @@
   | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
   | add_type_constraint _ _ = I
 
-fun repair_var_name s =
+fun repair_var_name_raw s =
   let
     fun subscript_name s n = s ^ nat_subscript n
     val s = s |> String.map Char.toLower
@@ -170,6 +170,11 @@
     | _ => s)
   end
 
+fun repair_var_name textual s =
+  (case unprefix_and_unascii schematic_var_prefix s of
+    SOME s => s
+  | NONE => s |> textual ? repair_var_name_raw)
+
 (* The number of type arguments of a constant, zero if it's monomorphic. For (instances of) Skolem
    pseudoconstants, this information is encoded in the constant name. *)
 fun robust_const_num_type_args thy s =
@@ -284,13 +289,10 @@
                 (case unprefix_and_unascii fixed_var_prefix s of
                   SOME s => Free (s, T)
                 | NONE =>
-                  (case unprefix_and_unascii schematic_var_prefix s of
-                    SOME s => Var ((s, var_index), T)
-                  | NONE =>
-                    if textual andalso not (is_tptp_variable s) then
-                      Free (s |> textual ? (repair_var_name #> fresh_up), T)
-                    else
-                      Var ((s |> textual ? repair_var_name, var_index), T)))
+                  if textual andalso not (is_tptp_variable s) then
+                    Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
+                  else
+                    Var ((repair_var_name textual s, var_index), T))
             in list_comb (t, ts) end))
   in do_term [] end
 
@@ -319,7 +321,7 @@
 
 fun quantify_over_var quant_of var_s t =
   let
-    val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
+    val vars = filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
     val normTs = vars |> AList.group (op =) |> map (apsnd hd)
     fun norm_var_types (Var (x, T)) =
         Var (x, (case AList.lookup (op =) normTs x of NONE => T | SOME T' => T'))
@@ -337,7 +339,7 @@
         do_formula pos (AQuant (q, xs, phi'))
         (* FIXME: TFF *)
         #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of)
-          (s |> textual ? repair_var_name)
+          (repair_var_name textual s)
       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
       | AConn (c, [phi1, phi2]) =>
         do_formula (pos |> c = AImplies ? not) phi1
@@ -589,10 +591,10 @@
           (case resolve_conjecture ss of
             [j] =>
             if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
-           | _ =>
-             (case resolve_fact fact_names ss of
-               [] => (ss, Plain, t)
-             | facts => (map fst facts, Axiom, t)))
+          | _ =>
+            (case resolve_fact fact_names ss of
+              [] => (ss, Plain, t)
+            | facts => (map fst facts, Axiom, t)))
       in
         ((num, ss'), role', t', rule, deps)
       end