# HG changeset patch
# User wenzelm
# Date 966501424 -7200
# Node ID de254f375477d823ecba4dac675f8baee85383f3
# Parent  3ade112482afdcc8452465dcc907d6704ef003dd
changed 'opaque' option to 'open' (opaque is default);
renamed 'mk_cases_tac' to 'ind_cases';

diff -r 3ade112482af -r de254f375477 src/HOL/Tools/induct_method.ML
--- 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;