equal
deleted
inserted
replaced
599 in ass (!calclist') : calcID end; |
599 in ass (!calclist') : calcID end; |
600 |
600 |
601 fun termopt2str (SOME t) = |
601 fun termopt2str (SOME t) = |
602 "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t) |
602 "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t) |
603 | termopt2str NONE = "NONE"; |
603 | termopt2str NONE = "NONE"; |
604 fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; |
604 (*fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; Isa2002*) |
|
605 (*Florian1009: 'val' would ensure static lookup, i.e. only at compile time; |
|
606 however, dynamic lookup is required, since "Isac" is not yet built here.*) |
|
607 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term |
|
608 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; |
|
609 |
605 fun terms2str ts= (strs2str o (map (Syntax.string_of_term |
610 fun terms2str ts= (strs2str o (map (Syntax.string_of_term |
606 (thy2ctxt' "Isac")))) ts; |
611 (thy2ctxt' "Isac")))) ts; |
607 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; |
612 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; |
608 val string_of_typ = type2str; |
613 val string_of_typ = type2str; |
609 |
614 |