# HG changeset patch
# User wenzelm
# Date 1132684486 -3600
# Node ID 8fde30f5cca6c9b973053363198ff3decab01a34
# Parent  699aad0746e2968930efb37f868c3dd95f1b6681
find_xxxS: term instead of thm;

diff -r 699aad0746e2 -r 8fde30f5cca6 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Tue Nov 22 19:34:44 2005 +0100
+++ b/src/Pure/Isar/induct_attrib.ML	Tue Nov 22 19:34:46 2005 +0100
@@ -25,11 +25,11 @@
   val lookup_coinductT : Proof.context -> string -> thm option
   val lookup_coinductS : Proof.context -> string -> thm option
   val find_casesT: Proof.context -> typ -> thm list
-  val find_casesS: Proof.context -> thm -> thm list
+  val find_casesS: Proof.context -> term -> thm list
   val find_inductT: Proof.context -> typ -> thm list
-  val find_inductS: Proof.context -> thm -> thm list
+  val find_inductS: Proof.context -> term -> thm list
   val find_coinductT: Proof.context -> typ -> thm list
-  val find_coinductS: Proof.context -> thm -> thm list
+  val find_coinductS: Proof.context -> term -> thm list
   val cases_type_global: string -> theory attribute
   val cases_set_global: string -> theory attribute
   val cases_type_local: string -> Proof.context attribute
@@ -180,11 +180,11 @@
   map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
 
 val find_casesT = find_rules (#1 o #1) encode_type;
-val find_casesS = find_rules (#2 o #1) Thm.concl_of;
+val find_casesS = find_rules (#2 o #1) I;
 val find_inductT = find_rules (#1 o #2) encode_type;
-val find_inductS = find_rules (#2 o #2) Thm.concl_of;
+val find_inductS = find_rules (#2 o #2) I;
 val find_coinductT = find_rules (#1 o #3) encode_type;
-val find_coinductS = find_rules (#2 o #3) Thm.concl_of;
+val find_coinductS = find_rules (#2 o #3) I;