When applied to a theorem A |- t, the function concl returns t.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# ADD_SYM;;
val it : thm = |- !m n. m + n = n + m
# concl ADD_SYM;;
val it : term = `!m n. m + n = n + m`
# concl (ASSUME `1 = 0`);;
val it : term = `1 = 0`