src/Tools/isac/Knowledge/Test.thy
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38015 67ba02dffacc
child 38034 928cebc9c4aa
     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) "",