# HG changeset patch
# User wenzelm
# Date 963481017 -7200
# Node ID be592460401075053019d9eacc2ce8f7327b3b93
# Parent  be6e79d1aae0e8e8f59e74a3bb3c7480f503398e
make: opaq flag;

diff -r be6e79d1aae0 -r be5924604010 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Jul 13 11:36:29 2000 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Thu Jul 13 11:36:57 2000 +0200
@@ -14,7 +14,7 @@
   val get: thm -> string list
   val add: thm -> thm * string list
   val none: thm -> thm * string list
-  val make: thm -> string list -> (string * T) list
+  val make: bool -> thm -> string list -> (string * T) list
   val rename_params: string list list -> thm -> thm
   val params: string list list -> 'a attribute
 end;
@@ -45,17 +45,18 @@
 
 (* prepare cases *)
 
-fun prep_case thm name i =
+fun prep_case opaq 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 = rename_wrt_term Bi (Logic.strip_params Bi);
+    val rev_params = map (if opaq then apfst Syntax.internal else I)
+      (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 thm names =
-  #1 (foldr (fn (name, (cases, i)) => (prep_case thm name i :: cases, i - 1))
+fun make opaq thm names =
+  #1 (foldr (fn (name, (cases, i)) => (prep_case opaq thm name i :: cases, i - 1))
     (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));