# HG changeset patch
# User blanchet
# Date 1406918669 -7200
# Node ID f1108245ba117551d1d4702770168fc8d8270037
# Parent  cac309e2b1f7a82920b7e65c9a793773c0330855
better handling of variable names

diff -r cac309e2b1f7 -r f1108245ba11 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Aug 01 20:15:41 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Aug 01 20:44:29 2014 +0200
@@ -30,6 +30,7 @@
 
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
+  val rename_bound_vars : term -> term
   val type_enc_aliases : (string * string list) list
   val unalias_type_enc : string -> string list
   val term_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc ->
@@ -101,6 +102,24 @@
     TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
   end
 
+fun single_letter upper s =
+  let val s' = if String.isPrefix "o" s orelse String.isPrefix "O" s then "z" else s in
+    String.extract (Name.desymbolize (SOME upper) (Long_Name.base_name s'), 0, SOME 1)
+  end
+
+fun var_name_of_typ (Type (@{type_name fun}, [_, T])) =
+    if body_type T = HOLogic.boolT then "p" else "f"
+  | var_name_of_typ (Type (@{type_name set}, [T])) = single_letter true (var_name_of_typ T)
+  | var_name_of_typ (Type (s, Ts)) =
+    if String.isSuffix "list" s then var_name_of_typ (the_single Ts) ^ "s"
+    else single_letter false (Long_Name.base_name s)
+  | var_name_of_typ (TFree (s, _)) = single_letter false (perhaps (try (unprefix "'")) s)
+  | var_name_of_typ (TVar ((s, _), T)) = var_name_of_typ (TFree (s, T))
+
+fun rename_bound_vars (t $ u) = rename_bound_vars t $ rename_bound_vars u
+  | rename_bound_vars (Abs (_, T, t)) = Abs (var_name_of_typ T, T, rename_bound_vars t)
+  | rename_bound_vars t = t
+
 exception ATP_CLASS of string list
 exception ATP_TYPE of string atp_type list
 exception ATP_TERM of (string, string atp_type) atp_term list
diff -r cac309e2b1f7 -r f1108245ba11 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 20:15:41 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 20:44:29 2014 +0200
@@ -210,18 +210,20 @@
 
         val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
 
-        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
+        val close_form_etc = rename_bound_vars o close_form
+
+        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form_etc
           | prop_of_clause names =
             let
-              val lits = map (HOLogic.dest_Trueprop o snd)
-                (map_filter (Symtab.lookup steps o fst) names)
+              val lits =
+                map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
             in
               (case List.partition (can HOLogic.dest_not) lits of
                 (negs as _ :: _, pos as _ :: _) =>
                 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
               | _ => fold (curry s_disj) lits @{term False})
             end
-            |> HOLogic.mk_Trueprop |> close_form
+            |> HOLogic.mk_Trueprop |> close_form_etc
 
         fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
 
@@ -350,8 +352,7 @@
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
-               #> relabel_isar_proof_nicely
-               #> rename_bound_vars_in_isar_proof)
+               #> relabel_isar_proof_nicely)
       in
         (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
           1 =>
diff -r cac309e2b1f7 -r f1108245ba11 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Aug 01 20:15:41 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Aug 01 20:44:29 2014 +0200
@@ -46,7 +46,6 @@
   val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
   val relabel_isar_proof_canonically : isar_proof -> isar_proof
   val relabel_isar_proof_nicely : isar_proof -> isar_proof
-  val rename_bound_vars_in_isar_proof : isar_proof -> isar_proof
 
   val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
 end;
@@ -207,34 +206,6 @@
     relabel_proof [] 0
   end
 
-val Type (listT_name, _) = HOLogic.listT dummyT
-
-fun var_name_of_typ (Type (@{type_name fun}, [_, T])) =
-    if body_type T = HOLogic.boolT then "p" else "f"
-  | var_name_of_typ (Type (@{type_name set}, [T])) =
-    Name.desymbolize (SOME true) (var_name_of_typ T)
-  | var_name_of_typ (Type (s, _)) =
-    if s = listT_name then "xs"
-    else String.extract (Name.desymbolize (SOME false) (Long_Name.base_name s), 0, SOME 1)
-  | var_name_of_typ (TFree (s, _)) =
-    String.extract (Name.desymbolize (SOME false) (perhaps (try (unprefix "'")) s), 0, SOME 1)
-  | var_name_of_typ (TVar ((s, _), T)) = var_name_of_typ (TFree (s, T))
-
-fun rename_bound_vars (t $ u) = rename_bound_vars t $ rename_bound_vars u
-  | rename_bound_vars (Abs (_, T, t)) = Abs (var_name_of_typ T, T, rename_bound_vars t)
-  | rename_bound_vars t = t
-
-val rename_bound_vars_in_isar_proof =
-  let
-    fun rename_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
-        Prove (qs, xs, l, rename_bound_vars t, map rename_proof subs, facts, meths, comment)
-      | rename_step step = step
-    and rename_proof (Proof (fix, assms, steps)) =
-      Proof (fix, map (apsnd rename_bound_vars) assms, map rename_step steps)
-  in
-    rename_proof
-  end
-
 val indent_size = 2
 
 fun string_of_isar_proof ctxt0 i n proof =