src/Pure/Isar/locale.ML
changeset 17438 e40afa461078
parent 17437 9deaf32c83be
child 17449 429ca1e21289
--- 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