src/Tools/isac/Interpret/script.sml
changeset 42362 b611f3c17af4
parent 42360 2c8de368c64c
child 42387 767debe8a50c
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Sat Jan 07 10:09:33 2012 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Sun Jan 08 08:41:35 2012 +0100
     1.3 @@ -567,7 +567,7 @@
     1.4  	           if f = f_ then Ass (m,f') else AssWeak (m,f')
     1.5  	         else NotAss
     1.6         | _ => NotAss)
     1.7 -
     1.8 +(*
     1.9    | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
    1.10      (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
    1.11        (tracing("### assod Check'_elementwise: consts= "^(term2str consts)^
    1.12 @@ -576,6 +576,12 @@
    1.13         if consts = consts'
    1.14         then (tracing"### assod Check'_elementwise: Ass"; Ass (m, consts_chkd))
    1.15         else (tracing"### assod Check'_elementwise: NotAss"; NotAss))
    1.16 +*)
    1.17 +  | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
    1.18 +    (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
    1.19 +      if consts = consts'
    1.20 +      then Ass (m, consts_chkd)
    1.21 +      else NotAss
    1.22  
    1.23    | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
    1.24  	    Ass (m, list)