# HG changeset patch
# User haftmann
# Date 1284551051 -7200
# Node ID e9cad160aa0f522436d1cbac8f12794e1c86f00c
# Parent  a1aa9fbcbd3db182a1140e3ab39b9fba08400982
dropped redundant normal_form command

diff -r a1aa9fbcbd3d -r e9cad160aa0f src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Sep 15 13:44:10 2010 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 15 13:44:11 2010 +0200
@@ -567,7 +567,7 @@
   in (nbe_program, idx_tab) end;
 
 
-(* evaluation oracle *)
+(* dynamic evaluation oracle *)
 
 fun mk_equals thy lhs raw_rhs =
   let
@@ -600,34 +600,9 @@
     (K (fn program => eval_term thy program (compile thy program)))));
 
 
-(* evaluation command *)
-
-fun norm_print_term ctxt modes t =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val t' = dynamic_eval_value thy t;
-    val ty' = Term.type_of t';
-    val ctxt' = Variable.auto_fixes t ctxt;
-    val p = Print_Mode.with_modes modes (fn () =>
-      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
-
-
-(** Isar setup **)
-
-fun norm_print_term_cmd (modes, s) state =
-  let val ctxt = Toplevel.context_of state
-  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
+(** setup **)
 
 val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
 
-val opt_modes =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-
-val _ =
-  Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
-    (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
-
 end;
  
\ No newline at end of file