src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

 
 structure Var_Set_Tab = Table(
   type key = indexname list
   val ord = list_ord Term_Ord.fast_indexname_ord)
 
-(* (1) Generalize Types *)
+(* (1) Generalize types *)
 fun generalize_types ctxt t =
   t |> map_types (fn _ => dummyT)
     |> Syntax.check_term
          (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
 
-(* (2) Typing-spot Table *)
+(* (2) Typing-spot table *)
 local
 fun key_of_atype (TVar (z, _)) =
     Ord_List.insert Term_Ord.fast_indexname_ord z
   | key_of_atype _ = I
 fun key_of_type T = fold_atyps key_of_atype T []

 in
 val typing_spot_table =
   post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
 end
 
-(* (3) Reverse-Greedy *)
+(* (3) Reverse-greedy *)
 fun reverse_greedy typing_spot_tab =
   let
     fun update_count z =
       fold (fn tvar => fn tab =>
         let val c = Vartab.lookup tab tvar |> the_default 0 in

         (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
         typing_spot_tab ([], Vartab.empty)
       |>> sort_distinct (rev_order o cost_ord o pairself snd)
   in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
 
-(* (4) Introduce Annotations *)
-fun introduce_annotations thy spots t t' =
-  let
+(* (4) Introduce annotations *)
+fun introduce_annotations ctxt spots t t' =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val get_types = post_fold_term_type (K cons) []
     fun match_types tp =
       fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
     fun unica' b x [] = if b then [x] else []
       | unica' b x (y :: ys) =

     val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
     fun erase_unica_tfrees env =
       let
         val unica =
           Vartab.fold (add_all_tfree_namesT o snd o snd) env []
+          |> filter_out (Variable.is_declared ctxt)
           |> unica fast_string_ord
         val erase_unica = map_atyps
           (fn T as TFree (s, _) =>
               if Ord_List.member fast_string_ord unica s then dummyT else T
             | T => T)

   in post_traverse_term_type post2 (0, rev annots) t |> fst end
 
 (* (5) Annotate *)
 fun annotate_types ctxt t =
   let
-    val thy = Proof_Context.theory_of ctxt
     val t' = generalize_types ctxt t
     val typing_spots =
       t' |> typing_spot_table
          |> reverse_greedy
          |> sort int_ord
-  in introduce_annotations thy typing_spots t t' end
+  in introduce_annotations ctxt typing_spots t t' end
 
 val indent_size = 2
 val no_label = ("", ~1)
 
 fun string_for_proof ctxt type_enc lam_trans i n =

       Vector.foldl
         ((fn (SOME t, (b, s)) => (b, Time.+ (t, s))
            | (NONE, (_, s)) => (true, Time.+ (preplay_timeout, s))) o apfst Lazy.force)
         (false, seconds 0.0)
 
-    (* Metis Preplaying *)
+    (* Metis preplaying *)
     fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) =
       if not preplay then (fn () => SOME (seconds 0.0)) else
         let
           val facts =
             fact_names