1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -44,13 +44,14 @@
     1.4  "--------------------- NTH ---------------------------------------------------";
     1.5  "--------------------- NTH ---------------------------------------------------";
     1.6  "--------------------- NTH ---------------------------------------------------";
     1.7 +val ctxt = Proof_Context.init_global @{theory}
     1.8  val prog_expr = assoc_rls "prog_expr"
     1.9  
    1.10  val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
    1.11  TermC.atomty t;
    1.12  val thm = Thm.prop_of @{thm NTH_NIL};
    1.13  TermC.atomty thm;
    1.14 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_NIL} t;
    1.15 +val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t;
    1.16  if UnparseC.term t' = "a" then () 
    1.17  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.18  
    1.19 @@ -65,16 +66,15 @@
    1.20  | _ => error "ListC.NTH changed";
    1.21  val thm = Thm.prop_of @{thm NTH_CONS};
    1.22  TermC.atomty thm;
    1.23 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false  @{thm NTH_CONS} t;
    1.24 +val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false  @{thm NTH_CONS} t;
    1.25  if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    1.26  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.27  
    1.28  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.29  val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
    1.30  TermC.atomty t;
    1.31 -Rewrite.trace_on := false; (*true false*)
    1.32 -val SOME (t', _) = rewrite_set_ thy false prog_expr t;
    1.33 -Rewrite.trace_on := false; (*true false*)
    1.34 +
    1.35 +val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
    1.36  if UnparseC.term t' = "c" then () 
    1.37  else error "NTH 3 [a,b,c,d,e] = c ..changed";
    1.38  
    1.39 @@ -85,25 +85,25 @@
    1.40  
    1.41  val thy = @{theory ListC};
    1.42  val t = TermC.str2term "Length [1, 1, 1]";
    1.43 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.44 +val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.45  UnparseC.term t = "1 + Length [1, 1]";
    1.46 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.47 +val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.48  UnparseC.term t = "1 + (1 + Length [1])";
    1.49 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.50 +val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.51  UnparseC.term t = "1 + (1 + (1 + Length []))";
    1.52 -val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.53 -val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.54 -val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.55 +val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.56 +val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.57 +val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
    1.58  if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    1.59  else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.60  
    1.61  val t = TermC.str2term "Length [1, 1, 1]";
    1.62 -val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
    1.63 +val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t;
    1.64  if UnparseC.term t = "3" then ()
    1.65  else error "Length [1, 1, 1] = 3  ..prog_expr changed";
    1.66  
    1.67  val t = TermC.str2term "Length [1, 1, 1]";
    1.68 -val t = eval_prog_expr thy prog_expr t;
    1.69 +val t = eval_prog_expr ctxt prog_expr t;
    1.70  case t of 
    1.71    Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () 
    1.72  | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";