1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  fun plural_s n = if n = 1 then "" else "s"
     1.6  
     1.7 -val serial_commas = ATP_Proof.serial_commas
     1.8 +val serial_commas = Try.serial_commas
     1.9  val simplify_spaces = ATP_Proof.strip_spaces false (K true)
    1.10  
    1.11  fun parse_bool_option option name s =
    1.12 @@ -231,7 +231,7 @@
    1.13      | NONE => raise Type.TYPE_MATCH
    1.14    end
    1.15  
    1.16 -val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    1.17 +val subgoal_count = Try.subgoal_count
    1.18  
    1.19  fun strip_subgoal ctxt goal i =
    1.20    let