# HG changeset patch
# User lcp
# Date 782556271 -3600
# Node ID 77474875da92c66640c18946e96e47e94a3200f8
# Parent  112cf8574cf1d06fd0cd6530bfda2dd4f7f8028b
LCF/fix/lfp_is_FIX: modified proof to suppress deep unification

diff -r 112cf8574cf1 -r 77474875da92 src/LCF/fix.ML
--- a/src/LCF/fix.ML	Wed Oct 19 09:41:48 1994 +0100
+++ b/src/LCF/fix.ML	Wed Oct 19 09:44:31 1994 +0100
@@ -49,11 +49,10 @@
 	(fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1,
 			stac (prem RS sym) 1, etac less_ap_term 1]);
 
-(*Generates unification messages for some reason*)
 val lfp_is_FIX = prove_goal LCF.thy
 	"[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)"
 	(fn [prem1,prem2] => [rtac less_anti_sym 1,
-			      rtac (FIX_eq RS (prem2 RS spec RS mp)) 1,
+			      rtac (prem2 RS spec RS mp) 1, rtac FIX_eq 1,
 			      rtac least_FIX 1, rtac prem1 1]);
 
 val ffix = read_instantiate [("f","f::?'a=>?'a")] FIX_eq;