equal
deleted
inserted
replaced
1046 val _ = use_text Output.ml_output false s |
1046 val _ = use_text Output.ml_output false s |
1047 in !eval_result end); |
1047 in !eval_result end); |
1048 |
1048 |
1049 fun print_evaluated_term s = Toplevel.keep (fn state => |
1049 fun print_evaluated_term s = Toplevel.keep (fn state => |
1050 let |
1050 let |
1051 val ctxt = Context.proof_of (Toplevel.context_of state); |
1051 val ctxt = Toplevel.context_of state; |
1052 val thy = ProofContext.theory_of ctxt; |
1052 val thy = ProofContext.theory_of ctxt; |
1053 val t = eval_term thy (ProofContext.read_term ctxt s); |
1053 val t = eval_term thy (ProofContext.read_term ctxt s); |
1054 val T = Term.type_of t; |
1054 val T = Term.type_of t; |
1055 in |
1055 in |
1056 writeln (Pretty.string_of |
1056 writeln (Pretty.string_of |