src/HOL/Code_Setup.thy
changeset 24835 8c26128f8997
parent 24463 841c2e24761f
child 24844 98c006a30218
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Oct 04 16:59:30 2007 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:41:49 2007 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  subsection {* Evaluation oracle *}
     1.5  
     1.6  oracle eval_oracle ("term") = {* fn thy => fn t => 
     1.7 -  if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) [] 
     1.8 +  if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
     1.9    then t
    1.10    else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    1.11  *}
    1.12 @@ -156,7 +156,7 @@
    1.13  
    1.14  method_setup normalization = {*
    1.15    Method.no_args (Method.SIMPLE_METHOD'
    1.16 -    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
    1.17 +    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
    1.18        THEN' resolve_tac [TrueI, refl]))
    1.19  *} "solve goal by normalization"
    1.20