501 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
501 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
502 | rls_of (Rewrite_Set rls) = rls |
502 | rls_of (Rewrite_Set rls) = rls |
503 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'"); |
503 | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'"); |
504 |
504 |
505 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = |
505 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = |
506 (thmID, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
506 (thmID, SOME ((subs2subst (assoc_thy "Isac") subs):subst)) |
507 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE) |
507 | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE) |
508 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE); |
508 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE); |
509 |
509 |
510 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) = |
510 fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) = |
511 (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
511 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst)) |
512 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE) |
512 | rls_of_rewset (Rewrite_Set rls) = (rls, NONE) |
513 | rls_of_rewset (Detail_Set rls) = (rls, NONE) |
513 | rls_of_rewset (Detail_Set rls) = (rls, NONE) |
514 | rls_of_rewset (Detail_Set_Inst (subs, rls)) = |
514 | rls_of_rewset (Detail_Set_Inst (subs, rls)) = |
515 (rls, SOME ((subs2subst (assoc_thy "Isac.thy") subs):subst)); |
515 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst)); |
516 |
516 |
517 fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID) |
517 fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID) |
518 | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm) |
518 | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm) |
519 | rule2tac subst (Thm (thmID, thm)) = |
519 | rule2tac subst (Thm (thmID, thm)) = |
520 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm)) |
520 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm)) |