1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Wed Apr 08 16:56:47 2020 +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", Rule.dummy_ord), 
     1.8 +  Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
     1.9      erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
    1.10      rules = [Rule_Def.Thm ("refl", TermC.num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    1.11         Rule_Def.Thm ("o_apply", TermC.num_str @{thm o_apply}),