diff -r cf398bb8a8be -r a80a35d67cf1 src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Wed Nov 15 17:05:44 2006 +0100
+++ b/src/HOL/ex/CodeEval.thy	Wed Nov 15 17:05:45 2006 +0100
@@ -122,8 +122,6 @@
   val eval_term: theory -> term -> term
   val term: string -> unit
   val eval_ref: term option ref
-  val oracle: string * (theory * exn -> term)
-  val method: Method.src -> Proof.context -> Method.method
 end;
 
 structure Eval : EVAL =
@@ -143,31 +141,9 @@
 
 exception Eval of term;
 
-val oracle = ("Eval", fn (thy, Eval t) =>
-  Logic.mk_equals (t, eval_term thy t));
-
-val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
-
-fun conv ct =
-  let
-    val {thy, t, ...} = rep_cterm ct;
-  in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
-
-fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
-  (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
-
-val method =
-  Method.no_args (Method.METHOD (fn _ =>
-    tac 1 THEN rtac TrueI 1));
-
 end;
 *}
 
-setup {*
-  Theory.add_oracle Eval.oracle
-  #> Method.add_method ("eval", Eval.method, "solve goal by evaluation")
-*}
-
 
 subsection {* Small examples *}
 
@@ -186,13 +162,4 @@
 
 ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
 
-lemma
-  "Suc 0 = 1" by eval
-
-lemma
-  "rev [0, Suc 0, Suc 0] = [Suc 0, Suc 0, 0]" by eval
-
-lemma
-  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval
-
 end
\ No newline at end of file