fix sml compilation
authornarboux
Wed Apr 25 15:38:56 2007 +0200 (2007-04-25)
changeset 227922443ae6dac7d
parent 22791 992222f3d2eb
child 22793 dc13dfd588b2
fix sml compilation
src/HOL/Nominal/nominal_fresh_fun.ML
     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