src/HOLCF/Sprod3.ML

         [
         (cut_facts_tac prems 1),
         (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
         (rtac sym 1),
         (rtac lub_chain_maxelem 1),
-        (res_inst_tac [("P","%j.Y(j)~=UU")] exE 1),
+        (res_inst_tac [("P","%j. Y(j)~=UU")] exE 1),
         (rtac (not_all RS iffD1) 1),
         (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
         (atac 1),
         (rtac chain_UU_I_inverse 1),
         (atac 1),

 (* ------------------------------------------------------------------------ *)
 (* convert all lemmas to the continuous versions                            *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "beta_cfun_sprod" thy [spair_def]
-        "(LAM x y.Ispair x y)`a`b = Ispair a b"
+        "(LAM x y. Ispair x y)`a`b = Ispair a b"
  (fn prems =>
         [
         (stac beta_cfun 1),
         (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1,
 					cont2cont_CF1L]) 1),

         ]);
 
 
 qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
 "[|is_chain(S)|] ==> range(S) <<| \
-\ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)"
+\ (| lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) |)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun_sprod 1),
         (stac (beta_cfun RS ext) 1),