1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 11:54:20 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 12:23:57 2021 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4  (*----------------------------- problem types --------------------------------*)
     1.5  (* ---------linear----------- *)
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Problem.prep_input thy "pbl_equ_univ_lin" [] Problem.id_empty
     1.8 +  [(Problem.prep_input @{theory} "pbl_equ_univ_lin" [] Problem.id_empty
     1.9        (["LINEAR", "univariate", "equation"],
    1.10          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.11            ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
    1.12 @@ -124,7 +124,7 @@
    1.13  
    1.14  (*-------------- methods------------------------------------------------------*)
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [MethodC.prep_input thy "met_eqlin" [] MethodC.id_empty
    1.17 +    [MethodC.prep_input @{theory} "met_eqlin" [] MethodC.id_empty
    1.18        (["LinEq"], [],
    1.19          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.20            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.21 @@ -148,7 +148,7 @@
    1.22    in
    1.23      Or_to_List e_e)"
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25 -    [MethodC.prep_input thy "met_eq_lin" [] MethodC.id_empty
    1.26 +    [MethodC.prep_input @{theory} "met_eq_lin" [] MethodC.id_empty
    1.27        (["LinEq", "solve_lineq_equation"],
    1.28          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.29            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),