1.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  val thy = @{theory "Biegelinie"};
     1.6  val ctxt = Proof_Context.init_global thy;
     1.7 -fun term2s t = UnparseC.term_in_ctxt ctxt t;
     1.8 +fun term2s t = UnparseC.term ctxt t;
     1.9  fun rewrit thm str = fst (the (rewrite_ ctxt tless_true Rule_Set.empty true thm str));
    1.10  
    1.11  "----------- the rules -------------------------------------------";
    1.12 @@ -74,10 +74,10 @@
    1.13  val M__ = ParseC.parse_test @{context}"M_b x = - 1 * x \<up> 2 / 2 + x * c + c_2";
    1.14  val SOME (e1__,_) = rewrite_set_ ctxt false prog_rls 
    1.15    (ParseC.parse_test @{context} "(NTH::[real,bool list]=>bool) 1 " $ rm_);
    1.16 -if UnparseC.term_in_ctxt @{context} e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
    1.17 +if UnparseC.term @{context} e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
    1.18  
    1.19  val SOME (x1__,_) = rewrite_set_ ctxt false prog_rls (ParseC.parse_test @{context} "argument_in (lhs (M_b 0 = 0))");
    1.20 -if UnparseC.term_in_ctxt @{context} x1__ = "0" then ()
    1.21 +if UnparseC.term @{context} x1__ = "0" then ()
    1.22  else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
    1.23  
    1.24