1.1 --- a/test/Tools/isac/Knowledge/rlang.sml	Tue Jul 20 14:37:56 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml	Tue Jul 27 11:21:14 2021 +0200
     1.3 @@ -186,9 +186,9 @@
     1.4  	 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
     1.5  
     1.6  (*WN---v *)
     1.7 -val bdv= TermC.parseNEW'' thy "bdv";
     1.8 -val v = TermC.parseNEW'' thy "x";
     1.9 -val t = TermC.parseNEW'' thy "3 * x / 5";
    1.10 +val bdv= (Thm.term_of o the o (TermC.parse thy)) "bdv";
    1.11 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
    1.12 +val t = (Thm.term_of o the o (TermC.parse thy)) "3 * x / 5";
    1.13  val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true 
    1.14  				    [ (bdv, v) ] make_ratpoly_in t;
    1.15  if UnparseC.term t' = "3 / 5 * x" then () else error "rlang.sml: 1";