# HG changeset patch
# User wenzelm
# Date 1164811486 -3600
# Node ID a3561bfe0ada6aa4619d078d29a83b030ec0c9a5
# Parent  8da782143bdea996a5242b32ef35aac33cee7c4a
simplified method setup;
tuned oracle setup;

diff -r 8da782143bde -r a3561bfe0ada src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Wed Nov 29 13:59:52 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Wed Nov 29 15:44:46 2006 +0100
@@ -68,7 +68,7 @@
 fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   (Drule.goals_conv (equal i) Codegen.evaluation_conv));
 val evaluation_meth =
-  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1));
+  Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI));
 
 in
 
@@ -135,7 +135,7 @@
 val oracle = ("Eval", fn (thy, Eval t) =>
   Logic.mk_equals (t, if eval_prop thy t then HOLogic.true_const else HOLogic.false_const));
 
-val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
+val oracle_name = Sign.full_name (the_context ()) (fst oracle);
 
 fun conv ct =
   let
@@ -146,8 +146,7 @@
   (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv)));
 
 val method =
-  Method.no_args (Method.METHOD (fn _ =>
-    tac 1 THEN rtac TrueI 1));
+  Method.no_args (Method.SIMPLE_METHOD' (tac THEN' rtac TrueI));
 
 end;
 *}
@@ -166,7 +165,7 @@
     (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
       NBE.normalization_conv)));
   val normalization_meth =
-    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
+    Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]));
 in
   Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
 end;