author | narboux |
Wed, 25 Apr 2007 15:38:56 +0200 | |
changeset 22792 | 2443ae6dac7d |
parent 22791 | 992222f3d2eb |
child 22793 | dc13dfd588b2 |
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Apr 25 15:26:01 2007 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Apr 25 15:38:56 2007 +0200 @@ -15,7 +15,7 @@ infix 1 THENL -fun (op THENL) (tac,tacs) = +fun tac THENL tacs = tac THEN (EVERY (map (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))