src/HOL/Tools/Nunchaku/nunchaku_collect.ML

       Spec_Rules.retrieve ctxt (Const x)
       |> sort (Spec_Rules.rough_classification_ord o apply2 #rough_classification);
 
     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
         let val card = card_of_type ctxt T in
           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
       else
         spec_rules ();