| changeset 24508 | c8b82fec6447 |
| parent 24493 | d4380e9b287b |
| child 24590 | 733120d04233 |
--- a/src/Tools/nbe.ML Sat Sep 01 01:22:11 2007 +0200 +++ b/src/Tools/nbe.ML Sat Sep 01 15:46:59 2007 +0200 @@ -377,9 +377,9 @@ (** Isar setup **) -fun norm_print_term_cmd (modes, raw_t) state = +fun norm_print_term_cmd (modes, s) state = let val ctxt = Toplevel.context_of state - in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end; + in norm_print_term ctxt modes (Syntax.read_term ctxt s) end; val setup = Theory.add_oracle ("normalization", normalization_oracle)