1.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -173,7 +173,7 @@
1.4 (*does a term contain a root ?*)
1.5 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy =
1.6 if strip_thy op0 <> "is'_root'_free"
1.7 - then raise error ("eval_root_free: wrong "^op0)
1.8 + then error ("eval_root_free: wrong "^op0)
1.9 else if const_in (strip_thy op0) arg
1.10 then SOME (mk_thmid thmid ""
1.11 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",