formal position for spec rule (not significant for equality);

--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Sun Dec 01 15:38:36 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Sun Dec 01 21:29:08 2019 +0100
@@ -500,7 +500,7 @@
 
     val specs =
       if s = \<^const_name>\<open>The\<close> then
-        [{name = "", rough_classification = Spec_Rules.Unknown,
+        [{pos = Position.none, name = "", rough_classification = Spec_Rules.Unknown,
           terms = [Logic.varify_global \<^term>\<open>The\<close>],
           rules = [@{thm theI_unique}]}]
       else if s = \<^const_name>\<open>finite\<close> then
@@ -508,7 +508,7 @@
           if card = Inf orelse card = Fin_or_Inf then
             spec_rules ()
           else
-            [{name = "", rough_classification = Spec_Rules.equational,
+            [{pos = Position.none, name = "", rough_classification = Spec_Rules.equational,
               terms = [Logic.varify_global \<^term>\<open>finite\<close>],
               rules = [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]}]
         end

--- a/src/Pure/Isar/spec_rules.ML	Sun Dec 01 15:38:36 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Sun Dec 01 21:29:08 2019 +0100
@@ -28,7 +28,11 @@
   val is_unknown: rough_classification -> bool
   val encode_rough_classification: rough_classification XML.Encode.T
   type spec =
-    {name: string, rough_classification: rough_classification, terms: term list, rules: thm list}
+   {pos: Position.T,
+    name: string,
+    rough_classification: rough_classification,
+    terms: term list,
+    rules: thm list}
   val get: Proof.context -> spec list
   val get_global: theory -> spec list
   val dest_theory: theory -> spec list
@@ -97,7 +101,11 @@
 (* rules *)
 
 type spec =
-  {name: string, rough_classification: rough_classification, terms: term list, rules: thm list};
+ {pos: Position.T,
+  name: string,
+  rough_classification: rough_classification,
+  terms: term list,
+  rules: thm list};
 
 fun eq_spec (specs: spec * spec) =
   (op =) (apply2 #name specs) andalso
@@ -105,8 +113,9 @@
   eq_list (op aconv) (apply2 #terms specs) andalso
   eq_list Thm.eq_thm_prop (apply2 #rules specs);
 
-fun map_spec_rules f ({name, rough_classification, terms, rules}: spec) : spec =
-  {name = name, rough_classification = rough_classification, terms = terms, rules = map f rules};
+fun map_spec_rules f ({pos, name, rough_classification, terms, rules}: spec) : spec =
+  {pos = pos, name = name, rough_classification = rough_classification, terms = terms,
+    rules = map f rules};
 
 structure Rules = Generic_Data
 (
@@ -150,7 +159,10 @@
 (* add *)
 
 fun add name rough_classification terms rules lthy =
-  let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
+  let
+    val pos = Position.thread_data ();
+    val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
+  in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => fn context =>
         let
@@ -162,14 +174,14 @@
             ||> map Thm.trim_context;
         in
           context |> (Rules.map o Item_Net.update)
-            {name = name, rough_classification = rough_classification,
+            {pos = pos, name = name, rough_classification = rough_classification,
               terms = terms', rules = rules'}
         end)
   end;
 
 fun add_global name rough_classification terms rules =
   (Context.theory_map o Rules.map o Item_Net.update)
-    {name = name, rough_classification = rough_classification,
+    {pos = Position.thread_data (), name = name, rough_classification = rough_classification,
       terms = terms, rules = map Thm.trim_context rules};
 
 end;

--- a/src/Pure/Thy/export_theory.ML	Sun Dec 01 15:38:36 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sun Dec 01 21:29:08 2019 +0100
@@ -402,15 +402,15 @@
 
     (* spec rules *)
 
-    fun encode_spec {name, rough_classification, terms, rules} =
+    fun encode_spec {pos, name, rough_classification, terms, rules} =
       let
         val terms' = map Logic.unvarify_global terms;
         val rules' = map (fn rule => #1 (standard_prop_of (prep_thm rule) NONE)) rules;
         open XML.Encode;
       in
-        pair string (pair Spec_Rules.encode_rough_classification
-          (pair (list encode_term) (list encode_prop)))
-          (name, (rough_classification, (terms', rules')))
+        pair properties (pair string (pair Spec_Rules.encode_rough_classification
+          (pair (list encode_term) (list encode_prop))))
+          (Position.properties_of pos, (name, (rough_classification, (terms', rules'))))
       end;
 
     val _ =

--- a/src/Pure/Thy/export_theory.scala	Sun Dec 01 15:38:36 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sun Dec 01 21:29:08 2019 +0100
@@ -711,13 +711,17 @@
 
 
   sealed case class Spec_Rule(
+    pos: Position.T,
     name: String,
     rough_classification: Rough_Classification,
     terms: List[Term.Term],
     rules: List[Prop])
   {
+    def id: Option[Long] = Position.Id.unapply(pos)
+
     def cache(cache: Term.Cache): Spec_Rule =
       Spec_Rule(
+        cache.position(pos),
         cache.string(name),
         rough_classification.cache(cache),
         terms.map(cache.term(_)),
@@ -731,10 +735,11 @@
     {
       import XML.Decode._
       import Term_XML.Decode._
-      list(pair(string, pair(decode_rough_classification, pair(list(term), list(decode_prop)))))(
-        body)
+      list(
+        pair(properties, pair(string, pair(decode_rough_classification,
+        pair(list(term), list(decode_prop))))))(body)
     }
-    for ((name, (rough_classification, (terms, rules))) <- spec_rules)
-      yield Spec_Rule(name, rough_classification, terms, rules)
+    for ((pos, (name, (rough_classification, (terms, rules)))) <- spec_rules)
+      yield Spec_Rule(pos, name, rough_classification, terms, rules)
   }
 }