1.1 --- a/src/HOL/Code_Generator.thy	Tue Mar 20 15:52:43 2007 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Tue Mar 20 17:07:23 2007 +0100
     1.3 @@ -185,40 +185,20 @@
     1.4  
     1.5  subsection {* Evaluation oracle *}
     1.6  
     1.7 -ML {*
     1.8 -structure HOL_Eval:
     1.9 -sig
    1.10 -  val reff: bool option ref
    1.11 -  val prop: theory -> term -> term
    1.12 -end =
    1.13 -struct
    1.14 -
    1.15 -val reff : bool option ref = ref NONE;
    1.16 -
    1.17 -fun prop thy t =
    1.18 -  if CodegenPackage.eval_term thy
    1.19 -    (("HOL_Eval.reff", reff), t)
    1.20 -    then HOLogic.true_const
    1.21 -    else HOLogic.false_const
    1.22 -
    1.23 -end
    1.24 -*}
    1.25 -
    1.26 -oracle eval_oracle ("term") = {*
    1.27 -  fn thy => fn t => Logic.mk_equals (t, HOL_Eval.prop thy t)
    1.28 +oracle eval_oracle ("term") = {* fn thy => fn t => 
    1.29 +  if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
    1.30 +  then t
    1.31 +  else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
    1.32  *}
    1.33  
    1.34  method_setup eval = {*
    1.35  let
    1.36 -
    1.37 -fun conv ct =
    1.38 -  let val {thy, t, ...} = rep_cterm ct
    1.39 -  in eval_oracle thy t end;
    1.40 -
    1.41 -fun eval_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.42 -  (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv)));
    1.43 -
    1.44 -in Method.no_args (Method.SIMPLE_METHOD' (eval_tac THEN' rtac TrueI)) end
    1.45 +  fun eval_tac thy = 
    1.46 +    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
    1.47 +in 
    1.48 +  Method.ctxt_args (fn ctxt => 
    1.49 +    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
    1.50 +end
    1.51  *} "solve goal by evaluation"
    1.52  
    1.53