src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
changeset 70496 be29e6fe82d8
parent 70494 41108e3e9ca5
equal deleted inserted replaced
70495:aaafff824632 70496:be29e6fe82d8
   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 thms' = thms |> map_index (uncurry (fn j =>
   225         val thms' = thms |> map_index (uncurry (fn j =>
   226           Thm.name_derivation
   226           Thm.name_derivation
   227             (((Long_Name.append qualifier base ^
   227             (((Long_Name.append qualifier base ^
   228               (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), Position.none))))
   228               (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), \<^here>))))
   229       in (local_name, thms') :: noted end
   229       in (local_name, thms') :: noted end
   230     else ((local_name, thms) :: name_noted_thms qualifier base noted);
   230     else ((local_name, thms) :: name_noted_thms qualifier base noted);
   231 
   231 
   232 fun substitute_noted_thm noted =
   232 fun substitute_noted_thm noted =
   233   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