src/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 42255 6201b34bd323
parent 42248 ac50595ffe6b
child 42281 19d9ab32a0ce
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Sep 07 12:55:28 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat Sep 10 10:37:24 2011 +0200
     1.3 @@ -1225,8 +1225,7 @@
     1.4  	             else Steps (ScrState is, ss))
     1.5  	
     1.6          | NasApp _ => NotLocatable
     1.7 -        | err => (writeln ("*** " ^ PolyML.makestring err); NotLocatable)
     1.8 -      end
     1.9 +        | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err)      end
    1.10  
    1.11    | locate_gen _ m _ (sc,_) (is, _) = 
    1.12        error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^