diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/thy-write.sml
--- a/src/Tools/isac/BaseDefinitions/thy-write.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/thy-write.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -12,7 +12,7 @@
   type authors
   datatype thydata
     = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
-    | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
+    | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rewrite_Ord.function}
     | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
     | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
     | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}