diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Fix.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -688,6 +688,43 @@
 	(etac cfun_arg_cong 1)
 	]);
 
+(* ------------------------------------------------------------------------- *)
+(* a result about functions with flat codomain                               *)
+(* ------------------------------------------------------------------------- *)
+
+val flat_codom = prove_goalw Fix.thy [flat_def]
+"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
+	(rtac disjI1 1),
+	(rtac UU_I 1),
+	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
+	(atac 1),
+	(rtac (minimal RS monofun_cfun_arg) 1),
+	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
+	(etac disjI1 1),
+	(rtac disjI2 1),
+	(rtac allI 1),
+	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
+	(atac 1),
+	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
+	(etac allE 1),(etac allE 1),
+	(dtac mp 1),
+	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(atac 1),
+	(etac allE 1),
+	(etac allE 1),
+	(dtac mp 1),
+	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(atac 1)
+	]);
+
 (* ------------------------------------------------------------------------ *)
 (* admissibility of special formulae and propagation                        *)
 (* ------------------------------------------------------------------------ *)
@@ -777,6 +814,8 @@
 	(etac spec 1)
 	]);
 
+val adm_all2 = (allI RS adm_all);
+
 val adm_subst = prove_goal  Fix.thy  
 	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
  (fn prems =>
@@ -1127,45 +1166,8 @@
 	]);
 
 
-val adm_all2 = (allI RS adm_all);
 
 val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
 	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
 	];
 
-(* ------------------------------------------------------------------------- *)
-(* a result about functions with flat codomain                               *)
-(* ------------------------------------------------------------------------- *)
-
-val flat_codom = prove_goalw Fix.thy [flat_def]
-"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
-	(rtac disjI1 1),
-	(rtac UU_I 1),
-	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
-	(atac 1),
-	(rtac (minimal RS monofun_cfun_arg) 1),
-	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
-	(etac disjI1 1),
-	(rtac disjI2 1),
-	(rtac allI 1),
-	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
-	(atac 1),
-	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
-	(etac allE 1),(etac allE 1),
-	(dtac mp 1),
-	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
-	(etac disjE 1),
-	(contr_tac 1),
-	(atac 1),
-	(etac allE 1),
-	(etac allE 1),
-	(dtac mp 1),
-	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
-	(etac disjE 1),
-	(contr_tac 1),
-	(atac 1)
-	]);