src/HOL/Tools/lin_arith.ML

     simpset = put_simpset HOL_basic_ss @{context} |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of,
     number_of = number_of});
 
 (* FIXME !?? *)
 fun add_arith_facts ctxt =
-  Simplifier.add_prems (Arith_Data.get_arith_facts ctxt) ctxt;
+  Simplifier.add_prems (Named_Theorems.get ctxt @{named_theorems arith}) ctxt;
 
 val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
 
 
 (* generic refutation procedure *)

   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup @{binding linarith}
     (Scan.succeed (fn ctxt =>
       METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
+        HEADGOAL (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" gen_tac;
 
 val setup =
   init_arith_data