# HG changeset patch
# User wenzelm
# Date 963481181 -7200
# Node ID 9ecb78a8d471ee2759f9943c65d0cfe7dd56af78
# Parent  3da2533e0a61c77f4b71190433e3b33bc8ac28fa
RuleCases.make opaq;

diff -r 3da2533e0a61 -r 9ecb78a8d471 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jul 13 11:39:22 2000 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jul 13 11:39:41 2000 +0200
@@ -41,7 +41,7 @@
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
   val resolveq_tac: thm Seq.seq -> int -> tactic
-  val resolveq_cases_tac: (thm * string list) Seq.seq
+  val resolveq_cases_tac: bool -> (thm * string list) Seq.seq
     -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
   val rule: thm list -> Proof.method
@@ -273,8 +273,8 @@
 
 val resolveq_tac = gen_resolveq_tac Tactic.rtac;
 
-val resolveq_cases_tac = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
-  Seq.map (rpair (RuleCases.make rule cases)) (Tactic.rtac rule i st));
+fun resolveq_cases_tac opaq = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
+  Seq.map (rpair (RuleCases.make opaq rule cases)) (Tactic.rtac rule i st));
 
 
 (* simple rule *)