src/Tools/isac/Interpret/calchead.sml
branchdecompose-isar
changeset 41950 2476f5f0f9ee
parent 41949 c1859b72ae8d
child 41951 50bc995aa45b
     1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Mon Apr 04 11:05:07 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Wed Apr 06 18:01:02 2011 +0200
     1.3 @@ -276,7 +276,7 @@
     1.4  
     1.5  (*.to an input (d,ts) find the according ori and insert the ts.*)
     1.6  (*WN.11.03: + dont take first inter<>[]*)
     1.7 -fun seek_oridts ctxt sel (d,ts) [] =
     1.8 +(*fun seek_oridts ctxt sel (d,ts) [] =
     1.9      ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
    1.10                               (comp_dts (d,ts))) ^
    1.11       "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
    1.12 @@ -286,6 +286,21 @@
    1.13  	 then ("", 
    1.14                 (id,vat,sel,d, inter op = ts ts'):ori, 
    1.15                 ts')
    1.16 +    else seek_oridts ctxt sel (d,ts) oris;*)
    1.17 +
    1.18 +fun seek_oridts ctxt sel (d,ts) [] =
    1.19 +    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
    1.20 +                             (comp_dts (d,ts))) ^
    1.21 +     "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
    1.22 +     [])
    1.23 +  | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
    1.24 +    if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
    1.25 +    then if sel = sel'
    1.26 +	 then ("", 
    1.27 +               (id,vat,sel,d, inter op = ts ts'):ori, 
    1.28 +               ts')
    1.29 +       else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))
    1.30 +         ^ " not for " ^ sel, e_ori_, [])
    1.31      else seek_oridts ctxt sel (d,ts) oris;
    1.32  
    1.33  (*.to an input (_,ts) find the according ori and insert the ts.*)