--- a/src/HOL/Tools/Transfer/transfer.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Thu Sep 09 12:33:14 2021 +0200
@@ -575,7 +575,7 @@
((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
in
thm
- |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
+ |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
@@ -596,7 +596,7 @@
((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
in
thm
- |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
+ |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
@@ -719,7 +719,7 @@
|> Raw_Simplifier.rewrite_rule ctxt' post_simps
|> Simplifier.norm_hhf ctxt'
|> Drule.generalize
- (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
+ (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
|> Drule.zero_var_indexes
end
(*
@@ -755,7 +755,7 @@
|> Raw_Simplifier.rewrite_rule ctxt' post_simps
|> Simplifier.norm_hhf ctxt'
|> Drule.generalize
- (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
+ (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
|> Drule.zero_var_indexes
end