src/HOL/UNITY/PPROD.ML

--- a/src/HOL/UNITY/PPROD.ML	Mon May 17 10:37:07 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Mon May 17 10:38:08 1999 +0200
@@ -62,7 +62,7 @@
 by Auto_tac;
 qed "PPROD_insert";
 
-Goalw [PPROD_def] "i : I ==> component (lift_prog i (F i)) (PPROD I F)";
+Goalw [PPROD_def] "i : I ==> (lift_prog i (F i)) component (PPROD I F)";
 (*blast_tac doesn't use HO unification*)
 by (fast_tac (claset() addIs [component_JN]) 1);
 qed "component_PPROD";