1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4            val hthm = Store.get (Data.get thy) theID theID
     1.5            val hthm' = Thy_Write.update_hthm hthm fillpats
     1.6              handle ERROR _ =>
     1.7 -              error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
     1.8 +              raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
     1.9          in Store.update theID theID hthm' end
    1.10      in Data.map (fold update_elem fis) thy end
    1.11  
    1.12 @@ -183,14 +183,14 @@
    1.13  
    1.14  fun assoc_calc thy calID = let
    1.15      fun ass ([], key) =
    1.16 -          error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
    1.17 +          raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
    1.18        | ass ((calc, (keyi, _)) :: pairs, key) =
    1.19            if key = keyi then calc else ass (pairs, key);
    1.20    in ass (thy |> KEStore_Elems.get_calcs, calID) end;
    1.21  
    1.22  fun assoc_calc' thy key = let
    1.23      fun ass ([], key') =
    1.24 -          error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
    1.25 +          raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
    1.26        | ass ((all as (keyi, _)) :: pairs, key') =
    1.27            if key' = keyi then all else ass (pairs, key');
    1.28    in ass (KEStore_Elems.get_calcs thy, key) end;