src/HOL/HOL.thy
changeset 55757 9fc71814b8c1
parent 55632 0f9d03649a9c
child 56375 32e0da92c786
     1.1 --- a/src/HOL/HOL.thy	Wed Feb 26 10:10:38 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Feb 26 11:57:52 2014 +0100
     1.3 @@ -1903,20 +1903,21 @@
     1.4  
     1.5  subsubsection {* Evaluation and normalization by evaluation *}
     1.6  
     1.7 -ML {*
     1.8 -fun eval_tac ctxt =
     1.9 -  let val conv = Code_Runtime.dynamic_holds_conv (Proof_Context.theory_of ctxt)
    1.10 -  in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    1.11 -*}
    1.12 -
    1.13 -method_setup eval = {* Scan.succeed (SIMPLE_METHOD' o eval_tac) *}
    1.14 -  "solve goal by evaluation"
    1.15 +method_setup eval = {*
    1.16 +let
    1.17 +  fun eval_tac ctxt =
    1.18 +    let val conv = Code_Runtime.dynamic_holds_conv ctxt
    1.19 +    in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    1.20 +in
    1.21 +  Scan.succeed (SIMPLE_METHOD' o eval_tac)
    1.22 +end
    1.23 +*} "solve goal by evaluation"
    1.24  
    1.25  method_setup normalization = {*
    1.26    Scan.succeed (fn ctxt =>
    1.27      SIMPLE_METHOD'
    1.28        (CHANGED_PROP o
    1.29 -        (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt))
    1.30 +        (CONVERSION (Nbe.dynamic_conv ctxt)
    1.31            THEN_ALL_NEW (TRY o rtac TrueI))))
    1.32  *} "solve goal by normalization"
    1.33