1.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml Thu Apr 29 17:05:11 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml Thu Apr 29 17:08:38 2021 +0200
1.3 @@ -160,19 +160,6 @@
1.4 | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
1.5 | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
1.6
1.7 -(* not only for thydata, but also for thy's etc *)
1.8 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
1.9 - | theID2guh [str] = part2guh [str]
1.10 - | theID2guh [s1, s2] = thy2guh [s1, s2]
1.11 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
1.12 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
1.13 - "Theorems" => thm2guh (isa, thyID) elemID
1.14 - | "Rulesets" => rls2guh (isa, thyID) elemID
1.15 - | "Calculations" => cal2guh (isa, thyID) elemID
1.16 - | "Orders" => ord2guh (isa, thyID) elemID
1.17 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
1.18 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
1.19 -
1.20 fun Html_default exist = (Html {guh = theID2guh exist,
1.21 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
1.22