--- a/src/HOL/Tools/TFL/rules.ML Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Mon Aug 08 17:23:15 2011 +0200
@@ -245,9 +245,7 @@
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
- fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
- aconv term_of atm)
- (#hyps(rep_thm th))
+ fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (Thm.hyps_of th)
val tml = Dcterm.strip_disj c
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1