src/Pure/Isar/locale.ML
changeset 17438 e40afa461078
parent 17437 9deaf32c83be
child 17449 429ca1e21289
equal deleted inserted replaced
17437:9deaf32c83be 17438:e40afa461078
  2410   in (propss, activate) end;
  2410   in (propss, activate) end;
  2411 
  2411 
  2412 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
  2412 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
  2413   map (rpair ([], [])) props);
  2413   map (rpair ([], [])) props);
  2414 
  2414 
  2415 fun prop_name thy propss =
  2415 fun goal_name thy kind target propss =
  2416     propss |> map (fn ((name, _), _) => extern thy name);
  2416     kind ^ Proof.goal_names (Option.map (extern thy) target) ""
  2417 fun goal_name thy kind NONE propss =
  2417       (propss |> map (fn ((name, _), _) => extern thy name));
  2418     kind ^ (Proof.goal_names NONE "" (prop_name thy propss))
       
  2419   | goal_name thy kind (SOME target) propss =
       
  2420     kind ^ (Proof.goal_names (SOME (extern thy target)) ""
       
  2421       (prop_name thy propss));
       
  2422 
  2418 
  2423 in
  2419 in
  2424 
  2420 
  2425 fun interpretation (prfx, atts) expr insts thy =
  2421 fun interpretation (prfx, atts) expr insts thy =
  2426   let
  2422   let