diff -r 46e6e1d91056 -r 198498f861ee src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -39,6 +39,8 @@
   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 mk_predT: typ list -> typ
   val mk_pred1T: typ -> typ
 
@@ -168,6 +170,9 @@
 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 mk_predT Ts = Ts ---> HOLogic.boolT;
 fun mk_pred1T T = mk_predT [T];