--- 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];