fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]

   | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =

 ((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)

      if k=k'

      then ((Ptyp (k', [pbt], ps))::pys)

      else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)

 	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))

 )			 

   | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =

 ((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)

      if k=k'

      then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)

      else 

 	 if length pys = 0

 	 then error ("insert: not found "^(strs2str (d:pblID)))

 	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))

 );

 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge

   function for trees / ptyps *)

 fun merge_ptyps ([], pt) = pt

   | merge_ptyps (pt, []) = pt

   | merge_ptyps ((Ptyp (k, x, ps)::xs), (ys' as Ptyp (k', y, ps')::ys)) =

       if k = k' then

         (Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)) else

         (Ptyp (k, x, ps) :: merge_ptyps (xs, ys'));