1.1 --- a/src/Tools/isac/MathEngBasic/method.sml	Tue Apr 27 19:52:29 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/method.sml	Wed Apr 28 12:38:13 2021 +0200
     1.3 @@ -50,32 +50,40 @@
     1.4        val gi = filter (eq "#Given") ppc;
     1.5        val gi = (case gi of
     1.6  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
     1.7 -		  | ((_, gi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'
     1.8 -		      handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
     1.9 +		  | ((_, gi') :: []) => 
    1.10 +        (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
    1.11 +          SOME x => x
    1.12 +        | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
    1.13  		  | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
    1.14  		  val gi = map (pair "#Given") gi;
    1.15  
    1.16  		  val fi = filter (eq "#Find") ppc;
    1.17  		  val fi = (case fi of
    1.18  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
    1.19 -		  | ((_, fi') :: []) =>  (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'
    1.20 -		      handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
    1.21 +		  | ((_, fi') :: []) => 
    1.22 +        (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
    1.23 +          SOME x => x
    1.24 +        | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
    1.25  		  | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
    1.26  		  val fi = map (pair "#Find") fi;
    1.27  
    1.28  		  val re = filter (eq "#Relate") ppc;
    1.29  		  val re = (case re of
    1.30  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
    1.31 -		  | ((_,re') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'
    1.32 -		      handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
    1.33 +		  | ((_,re') :: []) =>
    1.34 +        (case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
    1.35 +          SOME x => x
    1.36 +        | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
    1.37  		  | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
    1.38  		  val re = map (pair "#Relate") re;
    1.39  
    1.40  		  val wh = filter (eq "#Where") ppc;
    1.41  		  val wh = (case wh of
    1.42  		    [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
    1.43 -		  | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
    1.44 -		      handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
    1.45 +		  | ((_, wh') :: []) => 
    1.46 +        (case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of
    1.47 +          SOME x => x
    1.48 +        | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
    1.49  		  | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
    1.50  		  val sc = Program.prep_program scr
    1.51  		  val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc