1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -231,7 +231,7 @@
     1.4    | eval_var _ _ _ _ = NONE;
     1.5  
     1.6  fun lhs (Const ("HOL.eq",_) $ l $ _) = l
     1.7 -  | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
     1.8 +  | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
     1.9  (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)
    1.10  fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ = 
    1.11      SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
    1.12 @@ -246,7 +246,7 @@
    1.13  *)
    1.14  
    1.15  fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
    1.16 -  | rhs t = error("rhs called with (" ^ UnparseC.term t ^ ")");
    1.17 +  | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
    1.18  (*("rhs"    ,("Prog_Expr.rhs"    , eval_rhs "")):calc*)
    1.19  fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ = 
    1.20      SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
    1.21 @@ -485,7 +485,7 @@
    1.22     as the fst argument;
    1.23     this is, because Isabelles filter takes more than 1 sec.*)
    1.24  fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
    1.25 -  | same_funid f1 t = error ("same_funid called with t = ("
    1.26 +  | same_funid f1 t = raise ERROR ("same_funid called with t = ("
    1.27  		  ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
    1.28  (*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
    1.29  		   eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
    1.30 @@ -499,7 +499,7 @@
    1.31  | eval_filter_sameFunId _ _ _ _ = NONE;
    1.32  
    1.33  (* make a list of terms to a sum *)
    1.34 -fun list2sum [] = error ("list2sum called with []")
    1.35 +fun list2sum [] = raise ERROR ("list2sum called with []")
    1.36    | list2sum [s] = s
    1.37    | list2sum (s::ss) = 
    1.38      let