134 fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*) |
134 fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*) |
135 fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*) |
135 fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*) |
136 |
136 |
137 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) |
137 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*) |
138 (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) |
138 (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*) |
139 val ctxt_HOL = thy2ctxt' "Complex_Main"; |
139 (*val ctxt_HOL = thy2ctxt' "Complex_Main";*) |
140 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) |
140 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*) |
141 fun ctxt_Isac _ = thy2ctxt' "Isac"; |
141 (*fun ctxt_Isac _ = thy2ctxt' "Isac";*) |
142 fun Isac _ = ProofContext.theory_of (ctxt_Isac""); |
142 fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac"); |
143 |
143 |
144 val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" ); |
144 val e_rule = |
|
145 Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" ); |
145 fun id_of_thm (Thm (id, _)) = id |
146 fun id_of_thm (Thm (id, _)) = id |
146 | id_of_thm _ = raise error "id_of_thm"; |
147 | id_of_thm _ = raise error "id_of_thm"; |
147 fun thm_of_thm (Thm (_, thm)) = thm |
148 fun thm_of_thm (Thm (_, thm)) = thm |
148 | thm_of_thm _ = raise error "thm_of_thm"; |
149 | thm_of_thm _ = raise error "thm_of_thm"; |
149 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
150 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
597 |
598 |
598 (*fun termopt2str (SOME t) = |
599 (*fun termopt2str (SOME t) = |
599 "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t) |
600 "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t) |
600 | termopt2str NONE = "NONE";*) |
601 | termopt2str NONE = "NONE";*) |
601 fun termopt2str (SOME t) = |
602 fun termopt2str (SOME t) = |
602 "SOME " ^ (Syntax.string_of_term (ctxt_Isac"") t) |
603 "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t) |
603 | termopt2str NONE = "NONE"; |
604 | termopt2str NONE = "NONE"; |
604 fun term2str t = Syntax.string_of_term (ctxt_Isac"") t; |
605 fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; |
605 fun terms2str ts= (strs2str o (map (Syntax.string_of_term |
606 fun terms2str ts= (strs2str o (map (Syntax.string_of_term |
606 (ctxt_Isac"")))) ts; |
607 (thy2ctxt' "Isac")))) ts; |
607 (*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*) |
608 (*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*) |
608 fun type2str typ = Syntax.string_of_typ (ctxt_Isac"") typ; |
609 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; |
609 val string_of_typ = type2str; |
610 val string_of_typ = type2str; |
610 |
611 |
611 fun subst2str (s:subst) = |
612 fun subst2str (s:subst) = |
612 (strs2str o |
613 (strs2str o |
613 (map (linefeed o pair2str o |
614 (map (linefeed o pair2str o |