1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -185,12 +185,12 @@
     1.4  \<close> ML \<open>
     1.5  val id = ["univariate", "equation", "test"]
     1.6  \<close> ML \<open>
     1.7 -Problem.from_store_PIDE: Proof.context -> Problem.id -> Problem.T
     1.8 +Problem.from_store: Proof.context -> Problem.id -> Problem.T
     1.9  \<close> ML \<open>
    1.10  \<close> ML \<open> (* \<rightarrow> refine.sml*)
    1.11  \<close> ML \<open>
    1.12  \<close> text \<open>  local
    1.13 -refin_PIDE
    1.14 +refin
    1.15  \<close> ML \<open>
    1.16  \<close> text \<open>  \<isac_test>
    1.17  refine_PIDE
    1.18 @@ -201,19 +201,19 @@
    1.19  \<close> ML \<open>
    1.20  KEStore_Elems.get_pbls @{theory Poly}; (*! real ! due to Simplify :: "real => real" etc*)
    1.21  \<close> ML \<open>
    1.22 -Problem.from_store_PIDE @{context} ["polynomial", "simplification"]
    1.23 +Problem.from_store @{context} ["polynomial", "simplification"]
    1.24  \<close> ML \<open>
    1.25  val input = (["polynomial", "simplification"], 
    1.26    [("#Given", ["Simplify t_t"]), ("#Find", ["normalform n_n"])], 
    1.27    Rule_Set.empty, NONE (*cas*), 
    1.28    [["simplification","for_polynomials"]]) : Problem.input
    1.29  \<close> ML \<open>
    1.30 -Problem.prep_input_PIDE @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]
    1.31 +Problem.prep_input @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]
    1.32    input; (*! real !*)
    1.33  \<close> ML \<open>
    1.34  \<close> ML \<open>
    1.35  \<close> ML \<open>
    1.36 -"~~~~~ fun prep_input_PIDE , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =
    1.37 +"~~~~~ fun prep_input , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =
    1.38    (@{theory Poly}, "guh", ["math-author-1"], ["polynomial", "simplification"], input);
    1.39  \<close> ML \<open>
    1.40        fun eq f (f', _) = f = f';
    1.41 @@ -222,7 +222,7 @@
    1.42  \<close> ML \<open>
    1.43          val (_, gi') :: [] = (*case*) gi (*of*);
    1.44  \<close> ML \<open>
    1.45 -      map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) gi'
    1.46 +      map (Problem.split_did o (Syntax.read_term_global thy)) gi'
    1.47  \<close> ML \<open>
    1.48  \<close> ML \<open>
    1.49  (*+*)Syntax.read_term_global thy "Simplify t_t" (*Simplify :: "real => real"*)