211 if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated |
211 if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated |
212 | _ => raise ERROR ("associate: uncovered case")) |
212 | _ => raise ERROR ("associate: uncovered case")) |
213 | associate _ ctxt (tac, _) = |
213 | associate _ ctxt (tac, _) = |
214 (trace_msg_3 ctxt tac; Not_Associated); |
214 (trace_msg_3 ctxt tac; Not_Associated); |
215 |
215 |
216 (* find the next parent, which is either a PblObj xor a PrfObj in case of detail step*) |
216 (* in detail step find the next parent, which is either a PblObj xor a PrfObj *) |
217 fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty) |
217 fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty) |
218 | parent_node pt (pos as (p, _)) = |
218 | parent_node pt (pos as (p, _)) = |
219 let |
219 let |
220 fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty) |
220 fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty) |
221 | par pt p = |
221 | par pt p = |