Lines Matching defs:flatten
113 (* flatten let-expressions, leave no ``let ... = (let ... in ..) in ...`` *)
114 fun flatten (FUN_IF (x,t1,t2)) = FUN_IF (x, flatten t1, flatten t2)
115 | flatten (FUN_COND (x,t)) = FUN_COND (x, flatten t)
116 | flatten (FUN_VAL tm) = FUN_VAL tm
117 | flatten (FUN_LET (x,y,t)) = let
121 in foldr (fn ((x,y),z) => FUN_LET (x,y,z)) (flatten t) xs end
122 handle HOL_ERR _ => FUN_LET (x,y,flatten t)
124 val tm12 = ftree2tm (flatten (tm2ftree tm11))