equal
deleted
inserted
replaced
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.thy") subs):subst)); |
516 |
516 |
517 fun rule2tac (Thm (thmID, thm)) = |
517 fun rule2tac (Thm (thmID, thm)) = |
518 Rewrite (thmID, (de_quote o string_of_thm) thm) |
518 Rewrite (thmID, string_of_thmI thm) |
519 | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls) |
519 | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls) |
520 | rule2tac rule = |
520 | rule2tac rule = |
521 raise error ("rule2tac: called with '" ^ rule2str rule ^ "'"); |
521 raise error ("rule2tac: called with '" ^ rule2str rule ^ "'"); |
522 |
522 |
523 |
523 |