diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -131,7 +131,7 @@
 ML \<open>
 \<close> ML \<open>
 val prog_expr =
-  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
+  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
     erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
     rules = [Rule_Def.Thm ("refl",  @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
        Rule_Def.Thm ("o_apply",  @{thm o_apply}),