1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
     1.5          @{thm solve_linear_equation.simps})]
     1.6  \<close>
     1.7 -ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
     1.8 +ML \<open>Method.from_store' @{theory} ["LinEq","solve_lineq_equation"];\<close>
     1.9  
    1.10  end
    1.11