1.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml	Mon Jan 30 12:38:17 2023 +0100
     1.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml	Tue Jan 31 10:49:17 2023 +0100
     1.3 @@ -29,10 +29,10 @@
     1.4  val ctxt = ContextC.init_for_prog @{context} (vars t)
     1.5  
     1.6  (*----- now parsing infers the type *)
     1.7 -val SOME t = parseNEW ctxt "x";
     1.8 +val SOME t = ParseC.term_opt ctxt "x";
     1.9  if type_of t = HOLogic.realT then error "type inference failed 1" else ();
    1.10  
    1.11 -val SOME t = parseNEW ctxt "a";
    1.12 +val SOME t = ParseC.term_opt ctxt "a";
    1.13  if type_of t = HOLogic.realT then () else error "type inference failed 2";
    1.14  
    1.15  "----------- build fun initialise'--------------------------------------------------------------";
    1.16 @@ -45,7 +45,7 @@
    1.17  val (thy, fmz) = (@{theory Biegelinie}, fmz);
    1.18  
    1.19      val ctxt = thy |> Proof_Context.init_global
    1.20 -    val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct op =
    1.21 +    val ts = (map (ParseC.term_opt ctxt) fmz) |> map the |> map TermC.vars |> flat |> distinct op =
    1.22      val _ = TermC.raise_type_conflicts ts;
    1.23  
    1.24  "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";