1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -306,7 +306,7 @@
     1.4  fun guess_bdv_typ t = t |> vars |> hd |> type_of
     1.5  
     1.6  fun free2str (Free (s, _)) = s
     1.7 -  | free2str t = error ("free2str not for " ^ UnparseC.term t);
     1.8 +  | free2str t = raise ERROR ("free2str not for " ^ UnparseC.term t);
     1.9  fun str_of_free_opt (Free (s, _)) = SOME s
    1.10    | str_of_free_opt _ = NONE
    1.11  
    1.12 @@ -333,7 +333,7 @@
    1.13  
    1.14  fun isapair2pair (Const ("Product_Type.Pair",_) $ a $ b) = (a, b)
    1.15    | isapair2pair t = 
    1.16 -    error ("isapair2pair called with " ^ UnparseC.term t);
    1.17 +    raise ERROR ("isapair2pair called with " ^ UnparseC.term t);
    1.18  fun isalist2list ls =
    1.19    let
    1.20      fun get es (Const("List.list.Cons", _) $ t $ ls) = get (t :: es) ls
    1.21 @@ -490,15 +490,15 @@
    1.22  fun parseold thy str = (* before 2002 *)
    1.23    (let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str)
    1.24     in SOME (Thm.global_cterm_of thy t) end)
    1.25 -  handle _(*EXN? ..Inner syntax error Failed to parse term*) => NONE;
    1.26 +  handle _(*EXN? ..Inner syntax raise ERROR Failed to parse term*) => NONE;
    1.27  fun parseN thy str = (* introduced 2002 *)
    1.28    (let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.29     in SOME (Thm.global_cterm_of thy t) end)
    1.30 -  handle _(*EXN? ..Inner syntax error Failed to parse term*) => NONE;
    1.31 +  handle _(*EXN? ..Inner syntax raise ERROR Failed to parse term*) => NONE;
    1.32  fun parse thy str = (* introduced 2010 *)
    1.33    (let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)
    1.34     in SOME (Thm.global_cterm_of thy t) end)
    1.35 -  handle _(*EXN? ..Inner syntax error Failed to parse term*) => NONE;
    1.36 +  handle _(*EXN? ..Inner syntax raise ERROR Failed to parse term*) => NONE;
    1.37  
    1.38  (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
    1.39  fun parseNEW ctxt str = SOME (Syntax.read_term ctxt str |> numbers_to_string)