# HG changeset patch
# User narboux
# Date 1177508336 -7200
# Node ID 2443ae6dac7d9f1709dcde9c4d12a7a5731afbf9
# Parent  992222f3d2eb87aa2878e59292c94c3d1932a2e8
fix sml compilation

diff -r 992222f3d2eb -r 2443ae6dac7d src/HOL/Nominal/nominal_fresh_fun.ML
--- 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))))