diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/ProgLang/Prog_Expr.thy
--- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -263,13 +263,13 @@
 > reflI;
 val it = "(?t = ?t) = True"
 > val t = str2term "x = 0";
-> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
+> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
 
 > val t = str2term "1 = 0";
-> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
+> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
 ----------- thus needs Rule.Eval !
 > val t = str2term "0 = 0";
-> val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
+> val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
 > UnparseC.term t';
 val it = \<^const_name>\<open>True\<close>