219 val unfold_thms = Local_Defs.unfold0; |
219 val unfold_thms = Local_Defs.unfold0; |
220 |
220 |
221 fun name_noted_thms _ _ [] = [] |
221 fun name_noted_thms _ _ [] = [] |
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 (local_name, |
224 let |
225 map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^ |
225 val thms' = thms |> map_index (uncurry (fn j => |
226 (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted |
226 Thm.name_derivation |
227 else |
227 (((Long_Name.append qualifier base ^ |
228 ((local_name, thms) :: name_noted_thms qualifier base noted); |
228 (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), Position.none)))) |
|
229 in (local_name, thms') :: noted end |
|
230 else ((local_name, thms) :: name_noted_thms qualifier base noted); |
229 |
231 |
230 fun substitute_noted_thm noted = |
232 fun substitute_noted_thm noted = |
231 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 |
232 Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" |
234 Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" |
233 (perhaps (Termtab.lookup tab o Thm.full_prop_of) o Drule.zero_var_indexes) |
235 (perhaps (Termtab.lookup tab o Thm.full_prop_of) o Drule.zero_var_indexes) |