--- a/src/Pure/Proof/reconstruct.ML Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Proof/reconstruct.ML Thu Apr 27 15:06:35 2006 +0200
@@ -110,7 +110,7 @@
fun decompose sg Ts (env, p as (t, u)) =
let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify sg p
- else apsnd List.concat (foldl_map (decompose sg Ts) (uT env T U, ts ~~ us))
+ else apsnd flat (foldl_map (decompose sg Ts) (uT env T U, ts ~~ us))
in case pairself (strip_comb o Envir.head_norm env) p of
((Const c, ts), (Const d, us)) => rigrig c d (unifyT sg) ts us
| ((Free c, ts), (Free d, us)) => rigrig c d (unifyT sg) ts us