equal
deleted
inserted
replaced
119 fun name_multi name [x] = [(name, x)] |
119 fun name_multi name [x] = [(name, x)] |
120 | name_multi "" xs = map (pair "") xs |
120 | name_multi "" xs = map (pair "") xs |
121 | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
121 | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
122 |
122 |
123 fun name_thm pre official name thm = thm |
123 fun name_thm pre official name thm = thm |
124 |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) |
124 |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name |
125 |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name); |
125 |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name); |
126 |
126 |
127 fun name_thms pre official name xs = |
127 fun name_thms pre official name xs = |
128 map (uncurry (name_thm pre official)) (name_multi name xs); |
128 map (uncurry (name_thm pre official)) (name_multi name xs); |
129 |
129 |