--- a/src/HOL/Tools/induct_method.ML Thu Aug 17 10:35:49 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML Thu Aug 17 10:37:04 2000 +0200
@@ -234,7 +234,7 @@
val (thm', opt_cases') = foldr simp (1 upto Thm.nprems_of thm ~~ opt_cases, (thm, []));
in (thm', mapfilter I opt_cases') end;
-fun cases_tac (ctxt, ((simplified, opaque), args)) facts =
+fun cases_tac (ctxt, ((simplified, open_parms), args)) facts =
let
val sg = ProofContext.sign_of ctxt;
val cert = Thm.cterm_of sg;
@@ -272,7 +272,7 @@
fun prep_rule (thm, cases) =
Seq.map (cond_simp cases) (Method.multi_resolves facts [thm]);
- in Method.resolveq_cases_tac opaque (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
+ in Method.resolveq_cases_tac open_parms (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end;
in
@@ -331,7 +331,7 @@
end;
-fun induct_tac (ctxt, ((stripped, opaque), args)) facts =
+fun induct_tac (ctxt, ((stripped, open_parms), args)) facts =
let
val sg = ProofContext.sign_of ctxt;
val cert = Thm.cterm_of sg;
@@ -362,7 +362,8 @@
fun prep_rule (thm, cases) =
Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
- val tac = Method.resolveq_cases_tac opaque (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
+ val tac = Method.resolveq_cases_tac open_parms
+ (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
in
if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI])
else tac
@@ -383,7 +384,7 @@
val simplifiedN = "simplified";
val strippedN = "stripped";
-val opaqN = "opaque";
+val openN = "open";
val typeN = "type";
val setN = "set";
@@ -441,10 +442,10 @@
in
val cases_args = Method.syntax
- (mode simplifiedN -- mode opaqN -- (instss -- Scan.option cases_rule));
+ (mode simplifiedN -- mode openN -- (instss -- Scan.option cases_rule));
val induct_args = Method.syntax
- (mode strippedN -- mode opaqN -- (instss -- Scan.option induct_rule));
+ (mode strippedN -- mode openN -- (instss -- Scan.option induct_rule));
end;