src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
changeset 57793 d1cf76cef93b
parent 57792 9cb24c835284
child 58054 1d9edd486479
equal deleted inserted replaced
57792:9cb24c835284 57793:d1cf76cef93b
   216       |> (fn ((assms, steps), _) => Proof (fix, assms, steps))
   216       |> (fn ((assms, steps), _) => Proof (fix, assms, steps))
   217   in
   217   in
   218     relabel_proof [] 0
   218     relabel_proof [] 0
   219   end
   219   end
   220 
   220 
       
   221 fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s
       
   222 
   221 fun rationalize_obtains_in_isar_proofs ctxt =
   223 fun rationalize_obtains_in_isar_proofs ctxt =
   222   let
   224   let
   223     fun rename_obtains xs (subst, ctxt) =
   225     fun rename_obtains xs (subst, ctxt) =
   224       let
   226       let
   225         val Ts = map snd xs
   227         val Ts = map snd xs
   226         val new_names0 = map (prefix "some_" o var_name_of_typ o body_type) Ts
   228         val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts
   227         val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
   229         val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
   228         val ys = map2 pair new_names Ts
   230         val ys = map2 pair new_names Ts
   229       in
   231       in
   230         (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
   232         (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
   231       end
   233       end