# HG changeset patch
# User blanchet
# Date 1406916530 -7200
# Node ID e913a87bd5d2fd051cd7c0d956dbefe86e5d9a6c
# Parent  1649841f3b383de83daf5daea314d01a9ceb2fd5
nicer generated variable names

diff -r 1649841f3b38 -r e913a87bd5d2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 19:44:18 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 20:08:50 2014 +0200
@@ -350,7 +350,8 @@
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
-               #> relabel_isar_proof_nicely)
+               #> relabel_isar_proof_nicely
+               #> rename_bound_vars_in_isar_proof)
       in
         (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
           1 =>
diff -r 1649841f3b38 -r e913a87bd5d2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Aug 01 19:44:18 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Aug 01 20:08:50 2014 +0200
@@ -46,6 +46,7 @@
   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;
@@ -206,6 +207,34 @@
     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 =