--- a/src/Pure/logic.ML Mon Mar 16 23:39:44 2009 +0100
+++ b/src/Pure/logic.ML Mon Mar 16 23:52:30 2009 +0100
@@ -65,6 +65,7 @@
val flatten_params: int -> term -> term
val list_rename_params: string list * term -> term
val assum_pairs: int * term -> (term*term)list
+ val assum_problems: int * term -> (term -> term) * term list * term
val varifyT: typ -> typ
val unvarifyT: typ -> typ
val varify: term -> term
@@ -462,6 +463,13 @@
in pairrev (Hs,[])
end;
+fun assum_problems (nasms, A) =
+ let
+ val (params, A') = strip_assums_all ([], A)
+ val (Hs, B) = strip_assums_imp (nasms, [], A')
+ fun abspar t = rlist_abs (params, t)
+ in (abspar, rev Hs, B) end;
+
(* global schematic variables *)