src/Tools/nbe.ML
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)