1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -263,13 +263,13 @@
     1.4  > reflI;
     1.5  val it = "(?t = ?t) = True"
     1.6  > val t = str2term "x = 0";
     1.7 -> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
     1.8 +> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
     1.9  
    1.10  > val t = str2term "1 = 0";
    1.11 -> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
    1.12 +> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
    1.13  ----------- thus needs Rule.Eval !
    1.14  > val t = str2term "0 = 0";
    1.15 -> val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
    1.16 +> val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
    1.17  > UnparseC.term t';
    1.18  val it = \<^const_name>\<open>True\<close>
    1.19