src/HOL/Library/old_recdef.ML
changeset 60774 6c28d8ed2488
parent 60752 b48830b670a1
child 60781 2da59cdf531c
     1.1 --- a/src/HOL/Library/old_recdef.ML	Thu Jul 23 22:13:42 2015 +0200
     1.2 +++ b/src/HOL/Library/old_recdef.ML	Fri Jul 24 22:16:39 2015 +0200
     1.3 @@ -2550,7 +2550,7 @@
     1.4   *--------------------------------------------------------------------------*)
     1.5  fun std_postprocessor ctxt strict wfs =
     1.6    Prim.postprocess ctxt strict
     1.7 -   {wf_tac = REPEAT (ares_tac wfs 1),
     1.8 +   {wf_tac = REPEAT (ares_tac ctxt wfs 1),
     1.9      terminator =
    1.10        asm_simp_tac ctxt 1
    1.11        THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE