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