src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 28 18:54:18 2010 +0200
@@ -17,6 +17,7 @@
   val maybe_quote : string -> string
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
+  val subgoal_count : Proof.state -> int
   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
 end;
  
@@ -124,6 +125,8 @@
     | NONE => raise Type.TYPE_MATCH
   end
 
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
 fun strip_subgoal goal i =
   let
     val (t, frees) = Logic.goal_params (prop_of goal) i