# HG changeset patch # User wenzelm # Date 1575290042 -3600 # Node ID 39ccdbbed539312edf16025db987a163986ebcbf # Parent 475510f1a280b82016d8eae79c94deaebee7e833 more informative spec rules; diff -r 475510f1a280 -r 39ccdbbed539 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Dec 02 13:33:45 2019 +0100 +++ b/src/Pure/Isar/specification.ML Mon Dec 02 13:34:02 2019 +0100 @@ -216,6 +216,11 @@ val specs = map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls; + val spec_name = + Sign.full_name thy + (Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls)); + + (*consts*) val (consts, consts_thy) = thy |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls; @@ -229,7 +234,7 @@ (*facts*) val (facts, facts_lthy) = axioms_thy |> Named_Target.theory_init - |> Spec_Rules.add "" Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms) + |> Spec_Rules.add spec_name Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms) |> Local_Theory.notes axioms; in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;