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