604 (*fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; Isa2002*) |
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; |
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.*) |
606 however, dynamic lookup is required, since "Isac" is not yet built here.*) |
607 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term |
607 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term |
608 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; |
608 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; |
609 |
609 fun terms2str ts = (strs2str o (map term2str )) ts; |
610 fun terms2str ts= (strs2str o (map (Syntax.string_of_term |
610 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*) |
611 (thy2ctxt' "Isac")))) ts; |
611 fun terms2str' ts = (strs2str' o (map term2str )) ts; |
612 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; |
612 (*terms2str' [t1,t2] = "[1 + 2,abc]";*) |
|
613 fun terms2strs ts = (map term2str) ts; |
|
614 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*) |
|
615 |
|
616 un type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; |
613 val string_of_typ = type2str; |
617 val string_of_typ = type2str; |
614 |
618 |
615 fun subst2str (s:subst) = |
619 fun subst2str (s:subst) = |
616 (strs2str o |
620 (strs2str o |
617 (map (linefeed o pair2str o |
621 (map (linefeed o pair2str o |