equal
deleted
inserted
replaced
222 | name_noted_thms qualifier base ((local_name, thms) :: noted) = |
222 | name_noted_thms qualifier base ((local_name, thms) :: noted) = |
223 if Long_Name.base_name local_name = base then |
223 if Long_Name.base_name local_name = base then |
224 let |
224 let |
225 val name = Long_Name.append qualifier base; |
225 val name = Long_Name.append qualifier base; |
226 val pos = Position.thread_data (); |
226 val pos = Position.thread_data (); |
227 val thms' = thms |> map_index (uncurry (fn j => |
227 val thms' = |
228 Thm.name_derivation |
228 Thm_Name.list (name, pos) thms |> map (uncurry (Thm.name_derivation o Thm_Name.short)); |
229 (((name ^ (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), pos)))) |
|
230 in (local_name, thms') :: noted end |
229 in (local_name, thms') :: noted end |
231 else ((local_name, thms) :: name_noted_thms qualifier base noted); |
230 else ((local_name, thms) :: name_noted_thms qualifier base noted); |
232 |
231 |
233 fun substitute_noted_thm noted = |
232 fun substitute_noted_thm noted = |
234 let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in |
233 let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in |