src/Tools/isac/calcelems.sml
changeset 55428 2c1d7cd15e48
parent 55405 f6f755053660
child 55432 1780e9905d80
     1.1 --- a/src/Tools/isac/calcelems.sml	Thu Jun 05 15:49:44 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jun 05 16:41:42 2014 +0200
     1.3 @@ -484,7 +484,6 @@
     1.4  val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
     1.5  
     1.6  type thehier = (thydata ptyp) list;
     1.7 -val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
     1.8  (* required to determine sequence of main nodes of thehier in KEStore.thy *)
     1.9  fun part2guh ([str]:theID) =
    1.10      (case str of
    1.11 @@ -903,7 +902,7 @@
    1.12  
    1.13  fun coll_metguhs mets =
    1.14      let fun node coll (Ptyp (_,[n],ns)) =
    1.15 -	    [(#guh : met -> guh) n]
    1.16 +	    [(#guh : met -> guh) n] @ (nodes coll ns)
    1.17  	and nodes coll [] = coll
    1.18  	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
    1.19      in nodes [] mets end;