src/Pure/envir.ML

   else norm_term2 same (asol, iTs, t);
 
 val norm_term = gen_norm_term false;
 val norm_term_same = gen_norm_term true;
 
-val beta_norm = norm_term (empty 0);
+fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
 
 fun norm_type iTs = normTh iTs;
 fun norm_type_same iTs =
   if Vartab.is_empty iTs then raise SAME else normT iTs;