65 fun arguments_from_model ctxt mI itms = |
65 fun arguments_from_model ctxt mI itms = |
66 let |
66 let |
67 val mvat = Pre_Conds.max_variant itms |
67 val mvat = Pre_Conds.max_variant itms |
68 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b |
68 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b |
69 val itms = filter (okv mvat) itms |
69 val itms = filter (okv mvat) itms |
70 (** )fun itm2arg itms (_, (d, _)) = (*--- compare vvv----------------*) |
70 fun itm2arg _ (_, (_, _)) = [](*this limits errors to init_pstate, |
71 case find_first (test_dsc d) itms of |
|
72 NONE => raise ERROR (error_msg_2 ctxt d itms) |
|
73 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_ |
|
74 ( **)fun itm2arg _ (_, (_, _)) = [](*this limits errors to init_pstate, |
|
75 while changing I_Model.penvval_in triggers much more errors*) |
71 while changing I_Model.penvval_in triggers much more errors*) |
76 val pats = (#model o MethodC.from_store ctxt) mI |
72 val pats = (#model o MethodC.from_store ctxt) mI |
77 val _ = if pats = [] then raise ERROR error_msg_1 else () |
73 val _ = if pats = [] then raise ERROR error_msg_1 else () |
78 in (flat o (map (itm2arg itms))) pats end; |
74 in (flat o (map (itm2arg itms))) pats end; |
79 |
75 |