src/HOL/Library/Eval_Witness.thy
changeset 47432 e1576d13e933
parent 41472 f6ab14e61604
     1.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -77,8 +77,8 @@
     1.4  
     1.5  method_setup eval_witness = {*
     1.6    Scan.lift (Scan.repeat Args.name) >>
     1.7 -  (fn ws => K (SIMPLE_METHOD'
     1.8 -    (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
     1.9 +    (fn ws => K (SIMPLE_METHOD'
    1.10 +      (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
    1.11  *} "evaluation with ML witnesses"
    1.12  
    1.13