equal
deleted
inserted
replaced
539 |
539 |
540 (** Reading and printing terms wrt the current theory **) |
540 (** Reading and printing terms wrt the current theory **) |
541 |
541 |
542 fun top_sg() = #sign(rep_thm(topthm())); |
542 fun top_sg() = #sign(rep_thm(topthm())); |
543 |
543 |
544 fun read s = term_of (read_cterm (top_sg()) |
544 fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT)); |
545 (s, (TVar(("DUMMY",0),[])))); |
|
546 |
545 |
547 (*Print a term under the current signature of the proof state*) |
546 (*Print a term under the current signature of the proof state*) |
548 fun prin t = writeln (Sign.string_of_term (top_sg()) t); |
547 fun prin t = writeln (Sign.string_of_term (top_sg()) t); |
549 |
548 |
550 fun printyp T = writeln (Sign.string_of_typ (top_sg()) T); |
549 fun printyp T = writeln (Sign.string_of_typ (top_sg()) T); |