# HG changeset patch
# User wenzelm
# Date 973547653 -3600
# Node ID 998778f8d63bfec50918a179b33a8471b7341d29
# Parent  1820abac64fea11673154a124d12e80115f99e2a
make: open_parms argument;

diff -r 1820abac64fe -r 998778f8d63b src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Mon Nov 06 22:53:00 2000 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Mon Nov 06 22:54:13 2000 +0100
@@ -45,18 +45,18 @@
 
 (* prepare cases *)
 
-fun prep_case opaq thm name i =
+fun prep_case open_parms thm name i =
   let
     val (_, _, Bi, _) = Thm.dest_state (thm, i)
       handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
-    val rev_params = map (if opaq then apfst Syntax.internal else I)
+    val rev_params = map (if open_parms then I else apfst Syntax.internal)
       (rename_wrt_term Bi (Logic.strip_params Bi));
     val rev_frees = map Free rev_params;
     val props = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp Bi);
   in (name, (rev rev_params, props)) end;
 
-fun make opaq thm names =
-  #1 (foldr (fn (name, (cases, i)) => (prep_case opaq thm name i :: cases, i - 1))
+fun make open_parms thm names =
+  #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1))
     (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));