1.1 --- a/src/Tools/isac/calcelems.sml	Mon Jan 20 16:15:34 2014 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Tue Jan 21 00:27:44 2014 +0100
     1.3 @@ -800,6 +800,34 @@
     1.4  type ptyps = (pbt ptyp) list
     1.5  val ptyps = Unsynchronized.ref ([e_Ptyp] : ptyps);
     1.6  
     1.7 +
     1.8 +fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]
     1.9 +  | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
    1.10 +((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)
    1.11 +     if k=k'
    1.12 +     then ((Ptyp (k', [pbt], ps))::pys)
    1.13 +     else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
    1.14 +	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
    1.15 +)			 
    1.16 +  | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
    1.17 +((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)
    1.18 +     if k=k'
    1.19 +     then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
    1.20 +     else 
    1.21 +	 if length pys = 0
    1.22 +	 then error ("insert: not found "^(strs2str (d:pblID)))
    1.23 +	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
    1.24 +);
    1.25 +
    1.26 +(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
    1.27 +  function for trees / ptyps *)
    1.28 +fun merge_ptyps ([], pt) = pt
    1.29 +  | merge_ptyps (pt, []) = pt
    1.30 +  | merge_ptyps ((Ptyp (k, x, ps)::xs), (ys' as Ptyp (k', y, ps')::ys)) =
    1.31 +      if k = k' then
    1.32 +        (Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)) else
    1.33 +        (Ptyp (k, x, ps) :: merge_ptyps (xs, ys'));
    1.34 +
    1.35  (* types for methods *)
    1.36  
    1.37