--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Feb 17 13:31:42 2014 +0100
@@ -40,7 +40,7 @@
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
@@ -182,8 +182,7 @@
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];