1.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Aug 24 12:37:07 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Aug 24 17:21:14 2022 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  sig
     1.5    type authors
     1.6    datatype thydata
     1.7 -    = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
     1.8 +    = Hcal of {calc: Rule_Def.eval_ml_from_prog, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
     1.9      | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rewrite_Ord.function}
    1.10      | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
    1.11      | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
    1.12 @@ -54,7 +54,7 @@
    1.13  | Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
    1.14     thm: thm} (* here no sym_thm, thus no thmID required *)
    1.15  | Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
    1.16 -| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
    1.17 +| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.eval_ml_from_prog}
    1.18  | Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
    1.19      ord: (subst -> (term * term) -> bool)};
    1.20  fun the2str (Html {guh, ...}) = guh