src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 42094 e6867e9c6d10
parent 41228 e1fce873b814
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Mar 24 10:39:47 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Mar 24 15:29:31 2011 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val is_predT : typ -> bool
     1.5    val is_constrt : theory -> term -> bool
     1.6    val is_constr : Proof.context -> string -> bool
     1.7 +  val strip_ex : term -> (string * typ) list * term
     1.8    val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
     1.9    val strip_all : term -> (string * typ) list * term
    1.10    val strip_intro_concl : thm -> term * term list