equal
deleted
inserted
replaced
126 val mid = max_id itms; |
126 val mid = max_id itms; |
127 in add_idvat [] (mid + 1) mvat mis end; |
127 in add_idvat [] (mid + 1) mvat mis end; |
128 |
128 |
129 (* check a problem (ie. itm list) for matching a problemtype, |
129 (* check a problem (ie. itm list) for matching a problemtype, |
130 takes the Pre_Conds.max_variant for concluding completeness (could be another!) *) |
130 takes the Pre_Conds.max_variant for concluding completeness (could be another!) *) |
|
131 (* match_itms: theory -> I_Model.T -> Model_Pattern.T * unchecked * Rule_Def.rule_set -> |
|
132 bool * (I_Model.T * (bool * term) list)*) |
131 fun match_itms thy itms (pbt, where_, where_rls) = |
133 fun match_itms thy itms (pbt, where_, where_rls) = |
132 let |
134 let |
133 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b; |
135 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b; |
134 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *) |
136 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *) |
135 val mvat = Pre_Conds.max_variant itms'; |
137 val mvat = Pre_Conds.max_variant itms'; |