1.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -359,9 +359,10 @@
     1.4   TermC.parseNEW' ctxt str;
     1.5  
     1.6  "---------------";
     1.7 +val ctxt = @{context}
     1.8   val str = "x + 2*z";
     1.9   val t =  Syntax.read_term_global thy str;
    1.10 - val t = TermC.typ_a2real (Syntax.read_term_global thy str);
    1.11 + val t = Model_Pattern.adapt_term_to_type ctxt (Syntax.read_term_global thy str);
    1.12   Thm.global_cterm_of thy t;
    1.13   case TermC.parseNEW ctxt str of
    1.14     SOME t' => t'
    1.15 @@ -449,7 +450,7 @@
    1.16  "----- read_term_pattern ---";
    1.17  val t = (thy, str) |>> Proof_Context.init_global 
    1.18                      |-> Proof_Context.read_term_pattern;
    1.19 -val t_real = TermC.typ_a2real t;
    1.20 +val t_real = Model_Pattern.adapt_term_to_type ctxt t;
    1.21  if UnparseC.term_in_ctxt ctxt t_real =
    1.22    "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n        "
    1.23    ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n        "