src/Tools/nbe.ML
changeset 56925 601edd9a6859
parent 56920 d651b944c67e
child 56969 7491932da574
     1.1 --- a/src/Tools/nbe.ML	Fri May 09 08:13:36 2014 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri May 09 08:13:36 2014 +0200
     1.3 @@ -24,7 +24,6 @@
     1.4    val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
     1.5    val trace: bool Unsynchronized.ref
     1.6  
     1.7 -  val setup: theory -> theory
     1.8    val add_const_alias: thm -> theory -> theory
     1.9  end;
    1.10  
    1.11 @@ -617,9 +616,4 @@
    1.12        (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
    1.13    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    1.14  
    1.15 -
    1.16 -(** setup **)
    1.17 -
    1.18 -val setup = Value.add_evaluator ("nbe", dynamic_value);
    1.19 -
    1.20  end;