1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon May 11 11:22:46 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon May 11 11:38:52 2020 +0200
     1.3 @@ -494,13 +494,13 @@
     1.4  	          ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
     1.5  			end
     1.6      else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
     1.7 -  | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
     1.8 +  | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
     1.9  
    1.10  fun next_rule thy eval_rls ro [rs] t =
    1.11      let
    1.12        val der = Derive.do_one thy eval_rls rs ro NONE t;
    1.13      in case der of (_, r, _) :: _ => SOME r | _ => NONE end
    1.14 -  | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");
    1.15 +  | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
    1.16  
    1.17  fun attach_form (_: Rule.rule list list) (_: term) (_: term) = 
    1.18    [(*TODO*)]: ( Rule.rule * (term * term list)) list;
    1.19 @@ -556,7 +556,7 @@
    1.20  	        ((*tracing ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
    1.21  	        []) end
    1.22      else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
    1.23 -  | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
    1.24 +  | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
    1.25  
    1.26  fun next_rule thy eval_rls ro [rs] t =
    1.27      let val der = Derive.do_one thy eval_rls rs ro NONE t;
    1.28 @@ -565,7 +565,7 @@
    1.29  	      (_,r,_)::_ => SOME r
    1.30  	    | _ => NONE
    1.31      end
    1.32 -  | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");
    1.33 +  | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
    1.34  
    1.35  val pat0 = TermC.parse_patt thy "?r/?s+?u/?v :: real";
    1.36  val pat1 = TermC.parse_patt thy "?r/?s+?u    :: real";