src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 37995 06f02b15ef8a
parent 37962 d7dbe01f48d7
child 38019 e207a64e1e0b
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jul 26 14:14:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jul 26 17:03:21 2010 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val maybe_quote : string -> string
     1.5    val monomorphic_term : Type.tyenv -> term -> term
     1.6    val specialize_type : theory -> (string * typ) -> term -> term
     1.7 +  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
     1.8  end;
     1.9   
    1.10  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.11 @@ -126,5 +127,11 @@
    1.12      | NONE => raise Type.TYPE_MATCH
    1.13    end
    1.14  
    1.15 +fun strip_subgoal goal i =
    1.16 +  let
    1.17 +    val (t, frees) = Logic.goal_params (prop_of goal) i
    1.18 +    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
    1.19 +    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    1.20 +  in (rev (map dest_Free frees), hyp_ts, concl_t) end
    1.21  
    1.22  end;