1.1 --- a/src/Tools/isac/MathEngBasic/method.sml Tue Jul 20 14:37:56 2021 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Jul 27 11:21:14 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 (TermC.parseNEW'' thy)) gi'\<close> of
1.8 + (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse 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 (TermC.parseNEW'' thy)) fi'\<close> of
1.17 + (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse 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 (TermC.parseNEW'' thy)) re'\<close> of
1.26 + (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse 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));