src/HOLCF/Ssum1.ML

 	THEN (etac sym 1))
 
 in
 
 val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum(s1,s2) = (x << y)"
+"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum s1 s2 = (x << y)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac  select_equality 1),
 	(dtac conjunct1 2),

 	(simp_tac Cfun_ss 1)
 	]);
 
 
 val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = (x << y)"
+"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum s1 s2 = (x << y)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac  select_equality 1),
 	(dtac conjunct2 2),

 	(rtac refl_less 1)
 	]);
 
 
 val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = ((x::'a) = UU)"
+"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum s1 s2 = ((x::'a) = UU)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac  select_equality 1),
 	(rtac conjI 1),

 	(fast_tac HOL_cs 1)
 	]);
 
 
 val less_ssum1d = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinr(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x = UU)"
+"[|s1=Isinr(x); s2=Isinl(y)|] ==> less_ssum s1 s2 = (x = UU)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac  select_equality 1),
 	(dtac conjunct2 2),

 (* ------------------------------------------------------------------------ *)
 (* optimize lemmas about less_ssum                                          *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "less_ssum2a" Ssum1.thy 
-	"less_ssum(Isinl(x),Isinl(y)) = (x << y)"
+	"less_ssum (Isinl x) (Isinl y) = (x << y)"
  (fn prems =>
 	[
 	(rtac less_ssum1a 1),
 	(rtac refl 1),
 	(rtac refl 1)
 	]);
 
 qed_goal "less_ssum2b" Ssum1.thy 
-	"less_ssum(Isinr(x),Isinr(y)) = (x << y)"
+	"less_ssum (Isinr x) (Isinr y) = (x << y)"
  (fn prems =>
 	[
 	(rtac less_ssum1b 1),
 	(rtac refl 1),
 	(rtac refl 1)
 	]);
 
 qed_goal "less_ssum2c" Ssum1.thy 
-	"less_ssum(Isinl(x),Isinr(y)) = (x = UU)"
+	"less_ssum (Isinl x) (Isinr y) = (x = UU)"
  (fn prems =>
 	[
 	(rtac less_ssum1c 1),
 	(rtac refl 1),
 	(rtac refl 1)
 	]);
 
 qed_goal "less_ssum2d" Ssum1.thy 
-	"less_ssum(Isinr(x),Isinl(y)) = (x = UU)"
+	"less_ssum (Isinr x) (Isinl y) = (x = UU)"
  (fn prems =>
 	[
 	(rtac less_ssum1d 1),
 	(rtac refl 1),
 	(rtac refl 1)

 
 (* ------------------------------------------------------------------------ *)
 (* less_ssum is a partial order on ++                                     *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "refl_less_ssum" Ssum1.thy "less_ssum(p,p)"
+qed_goal "refl_less_ssum" Ssum1.thy "less_ssum p p"
  (fn prems =>
 	[
 	(res_inst_tac [("p","p")] IssumE2 1),
 	(hyp_subst_tac 1),
 	(rtac (less_ssum2a RS iffD2) 1),

 	(rtac (less_ssum2b RS iffD2) 1),
 	(rtac refl_less 1)
 	]);
 
 qed_goal "antisym_less_ssum" Ssum1.thy 
- "[|less_ssum(p1,p2);less_ssum(p2,p1)|] ==> p1=p2"
+ "[|less_ssum p1 p2; less_ssum p2 p1|] ==> p1=p2"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("p","p1")] IssumE2 1),
 	(hyp_subst_tac 1),

 	(etac (less_ssum2b RS iffD1) 1),
 	(etac (less_ssum2b RS iffD1) 1)
 	]);
 
 qed_goal "trans_less_ssum" Ssum1.thy 
- "[|less_ssum(p1,p2);less_ssum(p2,p3)|] ==> less_ssum(p1,p3)"
+ "[|less_ssum p1 p2; less_ssum p2 p3|] ==> less_ssum p1 p3"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("p","p1")] IssumE2 1),
 	(hyp_subst_tac 1),