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;