# HG changeset patch
# User berghofe
# Date 1044266766 -3600
# Node ID 16136d2da0db9273792d2164b4c9da95e459286d
# Parent  77614fe0936270b3d1868f3e790bb543ae1198d0
Moved find_intros_goal from goals.ML to pure_thy.ML

diff -r 77614fe09362 -r 16136d2da0db src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Feb 03 11:04:16 2003 +0100
+++ b/src/Pure/pure_thy.ML	Mon Feb 03 11:06:06 2003 +0100
@@ -31,6 +31,7 @@
   val thms_containing: theory -> string list * string list -> (string * thm list) list
   val thms_containing_consts: theory -> string list -> (string * thm) list
   val find_intros: theory -> term -> (string * thm) list
+  val find_intros_goal : theory -> thm -> int -> (string * thm) list
   val find_elims : theory -> term -> (string * thm) list
   val hide_thms: bool -> string list -> theory -> theory
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
@@ -248,6 +249,9 @@
 
 val find_intros = find_matching index_intros (Some o Logic.strip_imp_concl)
 
+fun find_intros_goal thy st i =
+  find_intros thy (Logic.concl_of_goal (prop_of st) i);
+
 val find_elims = find_matching index_elims
   (fn prop => case Logic.strip_imp_prems prop of [] => None | p::_ => Some p)