equal
deleted
inserted
replaced
714 |
714 |
715 (* get_thm(s) *) |
715 (* get_thm(s) *) |
716 |
716 |
717 fun retrieve_thms _ pick ctxt (Fact s) = |
717 fun retrieve_thms _ pick ctxt (Fact s) = |
718 let |
718 let |
719 val thy = theory_of ctxt; |
719 val th = Goal.prove ctxt [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt))) |
720 val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt))) |
|
721 handle ERROR msg => cat_error msg "Failed to retrieve literal fact."; |
720 handle ERROR msg => cat_error msg "Failed to retrieve literal fact."; |
722 in pick "" [th] end |
721 in pick "" [th] end |
723 | retrieve_thms from_thy pick ctxt xthmref = |
722 | retrieve_thms from_thy pick ctxt xthmref = |
724 let |
723 let |
725 val thy = theory_of ctxt; |
724 val thy = theory_of ctxt; |