src/HOL/Nominal/nominal_fresh_fun.ML
changeset 22792 2443ae6dac7d
parent 22787 85e7e32e6004
child 23054 d1bbe5afa279
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Apr 25 15:26:01 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Apr 25 15:38:56 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  infix 1 THENL
     1.6  
     1.7 -fun (op THENL) (tac,tacs) =
     1.8 +fun tac THENL tacs =
     1.9   tac THEN
    1.10    (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
    1.11