src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML

   val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
 
   val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
   val subst_nonatomic_types: (typ * typ) list -> term -> term
 
-  val lhs_heads_of : thm -> term list
+  val lhs_head_of : thm -> term
 
   val mk_predT: typ list -> typ
   val mk_pred1T: typ -> typ
 
   val mk_disjIN: int -> int -> thm

     in subst end;
 
 fun subst_nonatomic_types [] = I
   | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
 
-fun lhs_heads_of thm =
-  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
+fun lhs_head_of thm = Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))));
 
 fun mk_predT Ts = Ts ---> HOLogic.boolT;
 fun mk_pred1T T = mk_predT [T];
 
 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}