equal
deleted
inserted
replaced
55 |
55 |
56 (* retrieve *) |
56 (* retrieve *) |
57 |
57 |
58 fun retrieve_generic context = |
58 fun retrieve_generic context = |
59 Item_Net.retrieve (Rules.get context) |
59 Item_Net.retrieve (Rules.get context) |
60 #> (map o apsnd o apsnd o map) (Thm.transfer (Context.theory_of context)); |
60 #> (map o apsnd o apsnd o map) (Thm.transfer'' context); |
61 |
61 |
62 val retrieve = retrieve_generic o Context.Proof; |
62 val retrieve = retrieve_generic o Context.Proof; |
63 val retrieve_global = retrieve_generic o Context.Theory; |
63 val retrieve_global = retrieve_generic o Context.Theory; |
64 |
64 |
65 |
65 |