fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2)

 fun the_hier th ([]: (theID * thydata) list) = th

 fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)

   | the_hier th ((theID, thydata)::ths) =

   let

     if can_insert theID th 

     fun add_the th ((thydata, theID)) =

     then

       if can_insert theID th 

       then

         if exist_the theID th

         then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))

         else insrt theID thydata theID

       else

         let

           val th' = fill_parents th theID theID (*..*** insert: not found*)

           val th' = insrt theID thydata theID th'

         in merge_ptyps' th' end;

 in fold (add_the th) thes end

 fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =

   Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

     fillpats = fillpats', thm = thm}

   | update_hthm _ _ = raise ERROR "wrong data";

 (* for interface for dialog-authoring *)

 fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =

   let

     val rls' = 

       case rls of

         Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>

           Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

             calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

       | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>

             Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

               calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

       | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>

             Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,

               scr = scr, errpatts = errpatIDs}

       | Erls => Erls

   in

     Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

       thy_rls = (thyID, rls')}

   end

   | update_hrls _ _ = raise ERROR "wrong data";

 fun app_py p f (d:pblID) (k(*:pblRD*)) = let

     fun py_err _ =

           error ("app_py: not found: " ^ (strs2str d));

     fun app_py' _ [] = py_err ()

       | app_py' [] _ = py_err ()

       | app_py' [k0] ((p' as Ptyp (k', _, _  ))::ps) =

           if k0 = k' then f p' else app_py' [k0] ps

       | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =

           if k0 = k'' then app_py' ks ps else app_py' k' ps';

   in app_py' k p end;

 fun get_py p = let

         fun extract_py (Ptyp (_, [py], _)) = py

           | extract_py _ = error ("extract_py: Ptyp has wrong format.");

       in app_py p extract_py end;

 (*

 fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)

   let

     fun update_elem th (theID, fillpats) =

         val th' =

         val hthm = get_py th theID theID

           if exist_the theID th

         val hthm' = update_hthm hthm fillpats

           then (writeln ("*** insert: preserved " ^ strs2str theID); th)

           handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")

           else insrt theID thydata theID th

       in update_ptyps theID theID hthm' end

       in the_hier th' ths end

   in fold (update_elem th) fis end

     else

   *)

       let

         val th' = fill_parents th theID theID (*..*** insert: not found*)

         val th' = insrt theID thydata theID th'

       in the_hier th' ths end;