diff -r 2350ba2640fd -r aba19e46dd84 src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Fri Oct 07 20:46:48 2022 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Sat Oct 08 11:40:48 2022 +0200
@@ -185,12 +185,12 @@
 \<close> ML \<open>
 val id = ["univariate", "equation", "test"]
 \<close> ML \<open>
-Problem.from_store_PIDE: Proof.context -> Problem.id -> Problem.T
+Problem.from_store: Proof.context -> Problem.id -> Problem.T
 \<close> ML \<open>
 \<close> ML \<open> (* \<rightarrow> refine.sml*)
 \<close> ML \<open>
 \<close> text \<open>  local
-refin_PIDE
+refin
 \<close> ML \<open>
 \<close> text \<open>  \<isac_test>
 refine_PIDE
@@ -201,19 +201,19 @@
 \<close> ML \<open>
 KEStore_Elems.get_pbls @{theory Poly}; (*! real ! due to Simplify :: "real => real" etc*)
 \<close> ML \<open>
-Problem.from_store_PIDE @{context} ["polynomial", "simplification"]
+Problem.from_store @{context} ["polynomial", "simplification"]
 \<close> ML \<open>
 val input = (["polynomial", "simplification"], 
   [("#Given", ["Simplify t_t"]), ("#Find", ["normalform n_n"])], 
   Rule_Set.empty, NONE (*cas*), 
   [["simplification","for_polynomials"]]) : Problem.input
 \<close> ML \<open>
-Problem.prep_input_PIDE @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]
+Problem.prep_input @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]
   input; (*! real !*)
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
-"~~~~~ fun prep_input_PIDE , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =
+"~~~~~ fun prep_input , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =
   (@{theory Poly}, "guh", ["math-author-1"], ["polynomial", "simplification"], input);
 \<close> ML \<open>
       fun eq f (f', _) = f = f';
@@ -222,7 +222,7 @@
 \<close> ML \<open>
         val (_, gi') :: [] = (*case*) gi (*of*);
 \<close> ML \<open>
-      map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) gi'
+      map (Problem.split_did o (Syntax.read_term_global thy)) gi'
 \<close> ML \<open>
 \<close> ML \<open>
 (*+*)Syntax.read_term_global thy "Simplify t_t" (*Simplify :: "real => real"*)