src/Tools/nbe.ML
changeset 39396 e9cad160aa0f
parent 39392 7a0fcee7a2a3
child 39399 267235a14938
     1.1 --- a/src/Tools/nbe.ML	Wed Sep 15 13:44:10 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Wed Sep 15 13:44:11 2010 +0200
     1.3 @@ -567,7 +567,7 @@
     1.4    in (nbe_program, idx_tab) end;
     1.5  
     1.6  
     1.7 -(* evaluation oracle *)
     1.8 +(* dynamic evaluation oracle *)
     1.9  
    1.10  fun mk_equals thy lhs raw_rhs =
    1.11    let
    1.12 @@ -600,34 +600,9 @@
    1.13      (K (fn program => eval_term thy program (compile thy program)))));
    1.14  
    1.15  
    1.16 -(* evaluation command *)
    1.17 -
    1.18 -fun norm_print_term ctxt modes t =
    1.19 -  let
    1.20 -    val thy = ProofContext.theory_of ctxt;
    1.21 -    val t' = dynamic_eval_value thy t;
    1.22 -    val ty' = Term.type_of t';
    1.23 -    val ctxt' = Variable.auto_fixes t ctxt;
    1.24 -    val p = Print_Mode.with_modes modes (fn () =>
    1.25 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    1.26 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    1.27 -  in Pretty.writeln p end;
    1.28 -
    1.29 -
    1.30 -(** Isar setup **)
    1.31 -
    1.32 -fun norm_print_term_cmd (modes, s) state =
    1.33 -  let val ctxt = Toplevel.context_of state
    1.34 -  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
    1.35 +(** setup **)
    1.36  
    1.37  val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
    1.38  
    1.39 -val opt_modes =
    1.40 -  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
    1.41 -
    1.42 -val _ =
    1.43 -  Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
    1.44 -    (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
    1.45 -
    1.46  end;
    1.47   
    1.48 \ No newline at end of file