# 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 *)