1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4  
     1.5  fun primed (Const (id, T)) = Const (id ^ "'", T)
     1.6    | primed (Free (id, T)) = Free (id ^ "'", T)
     1.7 -  | primed t = raise error ("primed called with arg = '"^ term2str t ^"'");
     1.8 +  | primed t = error ("primed called with arg = '"^ term2str t ^"'");
     1.9  
    1.10  (*("primed", ("Diff.primed", eval_primed "#primed"))*)
    1.11  fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
    1.12 @@ -408,7 +408,7 @@
    1.13       ((term_of o the o (parse thy)) "derivative", 
    1.14        [(term_of o the o (parse thy)) "f_f'"])
    1.15       ]
    1.16 -  | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
    1.17 +  | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
    1.18  castab := 
    1.19  overwritel (!castab, 
    1.20  	    [((term_of o the o (parse thy)) "Diff",  
    1.21 @@ -426,7 +426,7 @@
    1.22       ((term_of o the o (parse thy)) "derivativeEq", 
    1.23        [(term_of o the o (parse thy)) "f_f'::bool"])
    1.24       ]
    1.25 -  | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
    1.26 +  | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
    1.27  castab := 
    1.28  overwritel (!castab, 
    1.29  	    [((term_of o the o (parse thy)) "Differentiate",