src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML

                               if tfree_name_trivial name then dummyT
                               else TFree (name, sort)))))
   in
     (t', subst)
   end
-
 
 (* (4) Typing-spot table *)
 local
 fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
   | key_of_atype _ = I