proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;

--- a/src/HOL/Library/Multiset.thy	Thu Mar 19 21:05:40 2009 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Mar 19 22:05:00 2009 +0100
@@ -1623,8 +1623,8 @@
     msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
     mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
     mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
-    smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1},
-    reduction_pair=@{thm ms_reduction_pair}
+    smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
+    reduction_pair= @{thm ms_reduction_pair}
   })
 end
 *}

--- a/src/HOL/Nominal/nominal_atoms.ML	Thu Mar 19 21:05:40 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Mar 19 22:05:00 2009 +0100
@@ -106,8 +106,8 @@
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               
-              val inj_type = @{typ nat}-->ak_type
-              val inj_on_type = inj_type-->(@{typ "nat set"})-->@{typ bool}  
+              val inj_type = @{typ nat} --> ak_type
+              val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool}
 
               (* first statement *)
               val stmnt1 = HOLogic.mk_Trueprop 

--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Mar 19 21:05:40 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Mar 19 22:05:00 2009 +0100
@@ -23,7 +23,7 @@
 val false_tm = @{cterm "False"};
 val zdvd1_eq = @{thm "zdvd1_eq"};
 val presburger_ss = @{simpset} addsimps [zdvd1_eq];
-val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac});
+val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
 
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;

--- a/src/HOLCF/Tools/domain/domain_library.ML	Thu Mar 19 21:05:40 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Thu Mar 19 22:05:00 2009 +0100
@@ -125,37 +125,37 @@
 infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
 infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
 infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
-infix 1 <<;     fun S <<  T = %%:@{const_name Porder.sq_le} $ S $ T;
+infix 1 <<;     fun S <<  T = %%: @{const_name Porder.sq_le} $ S $ T;
 infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
 
-infix 9 `  ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x;
+infix 9 `  ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
 infix 9 `% ; fun f`% s = f` %: s;
 infix 9 `%%; fun f`%%s = f` %%:s;
 
-fun mk_adm t = %%:@{const_name adm} $ t;
-fun mk_compact t = %%:@{const_name compact} $ t;
-val ID = %%:@{const_name ID};
-fun mk_strictify t = %%:@{const_name strictify}`t;
-fun mk_cfst t = %%:@{const_name cfst}`t;
-fun mk_csnd t = %%:@{const_name csnd}`t;
+fun mk_adm t = %%: @{const_name adm} $ t;
+fun mk_compact t = %%: @{const_name compact} $ t;
+val ID = %%: @{const_name ID};
+fun mk_strictify t = %%: @{const_name strictify}`t;
+fun mk_cfst t = %%: @{const_name cfst}`t;
+fun mk_csnd t = %%: @{const_name csnd}`t;
 (*val csplitN    = "Cprod.csplit";*)
 (*val sfstN      = "Sprod.sfst";*)
 (*val ssndN      = "Sprod.ssnd";*)
-fun mk_ssplit t = %%:@{const_name ssplit}`t;
-fun mk_sinl t = %%:@{const_name sinl}`t;
-fun mk_sinr t = %%:@{const_name sinr}`t;
-fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y;
-fun mk_up t = %%:@{const_name up}`t;
-fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u;
+fun mk_ssplit t = %%: @{const_name ssplit}`t;
+fun mk_sinl t = %%: @{const_name sinl}`t;
+fun mk_sinr t = %%: @{const_name sinr}`t;
+fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
+fun mk_up t = %%: @{const_name up}`t;
+fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
 val ONE = @{term ONE};
 val TT = @{term TT};
 val FF = @{term FF};
-fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z;
-fun mk_fix t = %%:@{const_name fix}`t;
-fun mk_return t = %%:@{const_name Fixrec.return}`t;
-val mk_fail = %%:@{const_name Fixrec.fail};
+fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
+fun mk_fix t = %%: @{const_name fix}`t;
+fun mk_return t = %%: @{const_name Fixrec.return}`t;
+val mk_fail = %%: @{const_name Fixrec.fail};
 
-fun mk_branch t = %%:@{const_name Fixrec.branch} $ t;
+fun mk_branch t = %%: @{const_name Fixrec.branch} $ t;
 
 val pcpoS = @{sort pcpo};
 
@@ -171,14 +171,14 @@
 fun cproj x      = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
 fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
-fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T);
+fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T);
 fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T;
-val UU = %%:@{const_name UU};
+infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T;
+val UU = %%: @{const_name UU};
 fun strict f = f`UU === UU;
 fun defined t = t ~= UU;
-fun cpair (t,u) = %%:@{const_name cpair}`t`u;
-fun spair (t,u) = %%:@{const_name spair}`t`u;
+fun cpair (t,u) = %%: @{const_name cpair}`t`u;
+fun spair (t,u) = %%: @{const_name spair}`t`u;
 fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
 |   mk_ctuple ts = foldr1 cpair ts;
 fun mk_stuple [] = ONE
@@ -186,7 +186,7 @@
 fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
 |   mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
 fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
-fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2;
+fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
 val mk_ctuple_pat = foldr1 cpair_pat;
 fun lift_defined f = lift (fn x => defined (f x));
 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);

--- a/src/ZF/Tools/inductive_package.ML	Thu Mar 19 21:05:40 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Mar 19 22:05:00 2009 +0100
@@ -231,12 +231,12 @@
      if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
      else all_tac,
      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
-                        ORELSE' eresolve_tac (asm_rl::@{thm PartE}::@{thm SigmaE2}::
+                        ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
                                               type_elims)
                         ORELSE' hyp_subst_tac)),
      if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
      else all_tac,
-     DEPTH_SOLVE (swap_res_tac (@{thm SigmaI}::@{thm subsetI}::type_intrs) 1)];
+     DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
 
   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   val mk_disj_rls = BalancedTree.accesses