equal
deleted
inserted
replaced
89 |
89 |
90 (** retrieve theorems **) |
90 (** retrieve theorems **) |
91 |
91 |
92 fun get_fact context thy xthmref = |
92 fun get_fact context thy xthmref = |
93 let |
93 let |
94 val ctxt = Context.proof_of context; |
|
95 |
|
96 val facts = facts_of thy; |
94 val facts = facts_of thy; |
97 val xname = Facts.name_of_ref xthmref; |
95 val xname = Facts.name_of_ref xthmref; |
98 val pos = Facts.pos_of_ref xthmref; |
96 val pos = Facts.pos_of_ref xthmref; |
99 |
97 |
100 val name = |
98 val name = |
105 val _ = Theory.check_thy thy; |
103 val _ = Theory.check_thy thy; |
106 in |
104 in |
107 (case res of |
105 (case res of |
108 NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) |
106 NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos) |
109 | SOME (static, ths) => |
107 | SOME (static, ths) => |
110 (Context_Position.report ctxt pos (Name_Space.markup (Facts.space_of facts) name); |
108 (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name); |
111 if static then () |
109 if static then () |
112 else Context_Position.report ctxt pos (Isabelle_Markup.dynamic_fact name); |
110 else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name); |
113 Facts.select xthmref (map (Thm.transfer thy) ths))) |
111 Facts.select xthmref (map (Thm.transfer thy) ths))) |
114 end; |
112 end; |
115 |
113 |
116 fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; |
114 fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; |
117 fun get_thm thy name = Facts.the_single name (get_thms thy name); |
115 fun get_thm thy name = Facts.the_single name (get_thms thy name); |