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