--- a/src/Pure/Isar/locale.ML Fri Sep 16 14:46:31 2005 +0200
+++ b/src/Pure/Isar/locale.ML Fri Sep 16 16:07:22 2005 +0200
@@ -2412,13 +2412,9 @@
fun prep_propp propss = propss |> map (fn ((name, _), props) =>
map (rpair ([], [])) props);
-fun prop_name thy propss =
- propss |> map (fn ((name, _), _) => extern thy name);
-fun goal_name thy kind NONE propss =
- kind ^ (Proof.goal_names NONE "" (prop_name thy propss))
- | goal_name thy kind (SOME target) propss =
- kind ^ (Proof.goal_names (SOME (extern thy target)) ""
- (prop_name thy propss));
+fun goal_name thy kind target propss =
+ kind ^ Proof.goal_names (Option.map (extern thy) target) ""
+ (propss |> map (fn ((name, _), _) => extern thy name));
in