1.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Mon Jul 19 18:39:02 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Tue Jul 20 14:37:56 2021 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4        val gi = (case gi of
     1.5  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
     1.6  		  | ((_, gi') :: []) => 
     1.7 -        (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
     1.8 +        (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) gi'\<close> of
     1.9            SOME x => x
    1.10          | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
    1.11  		  | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
    1.12 @@ -64,7 +64,7 @@
    1.13  		  val fi = (case fi of
    1.14  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
    1.15  		  | ((_, fi') :: []) => 
    1.16 -        (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
    1.17 +        (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) fi'\<close> of
    1.18            SOME x => x
    1.19          | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
    1.20  		  | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
    1.21 @@ -74,7 +74,7 @@
    1.22  		  val re = (case re of
    1.23  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
    1.24  		  | ((_,re') :: []) =>
    1.25 -        (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
    1.26 +        (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) re'\<close> of
    1.27            SOME x => x
    1.28          | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
    1.29  		  | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));