equal
deleted
inserted
replaced
139 | NoMatch' of P_Model.T; |
139 | NoMatch' of P_Model.T; |
140 |
140 |
141 (* match a formalization with a problem type, for tests *) |
141 (* match a formalization with a problem type, for tests *) |
142 fun match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) = |
142 fun match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) = |
143 let |
143 let |
144 val oris = O_Model.init thy fmz model(* |> #1*); |
144 val (oris, _) = O_Model.init thy fmz model(* |> #1*); |
145 val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er); |
145 val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er); |
146 in |
146 in |
147 if bool |
147 if bool |
148 then Matches' (P_Model.from thy itms where_') |
148 then Matches' (P_Model.from thy itms where_') |
149 else NoMatch' (P_Model.from thy itms where_') |
149 else NoMatch' (P_Model.from thy itms where_') |