1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Sep 05 12:40:23 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Sep 07 10:07:13 2011 +0200
     1.3 @@ -1,9 +1,10 @@
     1.4 -(* interpreter for scripts
     1.5 -   (c) Walther Neuper 2000
     1.6 +(* Title:  interpreter for scripts
     1.7 +   Author: Walther Neuper 2000
     1.8 +   (c) due to copyright terms
     1.9 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.10 +        10        20        30        40        50        60        70        80
    1.11 +*)
    1.12  
    1.13 -use"ME/script.sml";
    1.14 -use"script.sml";
    1.15 -*)
    1.16  signature INTERPRETER =
    1.17  sig
    1.18    (*type ets (list of executed tactics) see sequent.sml*)
    1.19 @@ -565,12 +566,12 @@
    1.20  
    1.21    | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
    1.22      (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
    1.23 -      ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
    1.24 +      (tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
    1.25  	     ", consts'= "^(term2str consts'));
    1.26 -       atomty consts; atomty consts';*)
    1.27 +       atomty consts; atomty consts';
    1.28         if consts = consts'
    1.29 -       then ((*tracing"### assod Check'_elementwise: Ass";*) Ass (m, consts_chkd))
    1.30 -       else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss))
    1.31 +       then (tracing"### assod Check'_elementwise: Ass"; Ass (m, consts_chkd))
    1.32 +       else (tracing"### assod Check'_elementwise: NotAss"; NotAss))
    1.33  
    1.34    | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
    1.35  	    Ass (m, list) 
    1.36 @@ -1224,6 +1225,7 @@
    1.37  	             else Steps (ScrState is, ss))
    1.38  	
    1.39          | NasApp _ => NotLocatable
    1.40 +        | err => (writeln ("*** " ^ PolyML.makestring err); NotLocatable)
    1.41        end
    1.42  
    1.43    | locate_gen _ m _ (sc,_) (is, _) =