1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sun Apr 18 23:40:30 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sun Apr 18 23:45:45 2021 +0200
     1.3 @@ -497,21 +497,20 @@
     1.4  
     1.5  (* TODO clarify parse with Test_Isac *)
     1.6  fun parseold thy str = (* before 2002 *)
     1.7 -  (let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str)
     1.8 -   in SOME (Thm.global_cterm_of thy t) end)
     1.9 -  handle _(*EXN? ..Inner syntax raise ERROR Failed to parse term*) => NONE;
    1.10 +  \<^try>\<open>
    1.11 +    let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str)
    1.12 +    in Thm.global_cterm_of thy t end\<close>;
    1.13  fun parseN thy str = (* introduced 2002 *)
    1.14 -  (let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.15 -   in SOME (Thm.global_cterm_of thy t) end)
    1.16 -  handle _(*EXN? ..Inner syntax raise ERROR Failed to parse term*) => NONE;
    1.17 +  \<^try>\<open>
    1.18 +    let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.19 +    in Thm.global_cterm_of thy t end\<close>;
    1.20  fun parse thy str = (* introduced 2010 *)
    1.21 -  (let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)
    1.22 -   in SOME (Thm.global_cterm_of thy t) end)
    1.23 -  handle _(*EXN? ..Inner syntax raise ERROR Failed to parse term*) => NONE;
    1.24 +  \<^try>\<open>
    1.25 +    let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)
    1.26 +    in Thm.global_cterm_of thy t end\<close>;
    1.27  
    1.28  (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
    1.29 -fun parseNEW ctxt str = SOME (Syntax.read_term ctxt str |> numbers_to_string)
    1.30 -   handle _ => NONE;
    1.31 +fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str |> numbers_to_string\<close>;
    1.32  fun parseNEW' ctxt str = 
    1.33    case parseNEW ctxt str of
    1.34      SOME t => t