src/Pure/Isar/method.ML
changeset 23178 07ba6b58b3d2
parent 23086 12320f6e2523
child 23349 23a8345f89f5
     1.1 --- a/src/Pure/Isar/method.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -216,7 +216,8 @@
     1.4  local
     1.5  
     1.6  fun asm_tac ths =
     1.7 -  foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
     1.8 +  fold_rev (curry op APPEND')
     1.9 +    (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths) (K no_tac);
    1.10  
    1.11  fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
    1.12    if cond (Logic.strip_assums_concl prop)