avoid renaming of params in cases;

--- a/src/Pure/Isar/proof.ML	Tue Jan 09 15:15:28 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Jan 09 15:17:08 2001 +0100
@@ -130,7 +130,7 @@
   Theorem of theory attribute list |    (*top-level theorem*)
   Lemma of theory attribute list |      (*top-level lemma*)
   Show of context attribute list |      (*intermediate result, solving subgoal*)
-  Have of context attribute list ;       (*intermediate result*)
+  Have of context attribute list ;      (*intermediate result*)
 
 val kind_name =
   fn Theorem _ => "theorem" | Lemma _ => "lemma" | Show _ => "show" | Have _ => "have";
@@ -548,12 +548,12 @@
 
 fun invoke_case (name, atts) state =
   let
-    val (fixes, lets, asms) = ProofContext.apply_case (context_of state) (get_case state name);
+    val (state', (lets, asms)) =
+      map_context_result (ProofContext.apply_case (get_case state name)) state;
   in
-    state
-    |> fix_i (map (fn (x, T) => ([x], Some T)) fixes)
+    state'
     |> add_binds_i lets
-    |> assume_i [((name, atts), map (fn t => (t, ([], []))) asms)]
+    |> assume_i [((name, atts), map (rpair ([], [])) asms)]
   end;
 
 

--- a/src/Pure/Isar/proof_context.ML	Tue Jan 09 15:15:28 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 09 15:17:08 2001 +0100
@@ -90,8 +90,7 @@
   val bind_skolem: context -> string list -> term -> term
   val get_case: context -> string -> RuleCases.T
   val add_cases: (string * RuleCases.T) list -> context -> context
-  val apply_case: context -> RuleCases.T
-    -> (string * typ) list * (indexname * term option) list * term list
+  val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
   val show_hyps: bool ref
   val pretty_thm: thm -> Pretty.T
   val verbose: bool ref
@@ -1019,11 +1018,12 @@
 
 (* local contexts *)
 
-fun apply_case ctxt ({fixes, assumes, binds}: RuleCases.T) =
+fun apply_case ({fixes, assumes, binds}: RuleCases.T) ctxt =
   let
-    val xs = map (bind_skolem ctxt (map #1 fixes) o Free) fixes;
+    fun bind (c, (x, T)) = (c |> fix_i [([x], Some T)], bind_skolem c [x] (Free (x, T)));
+    val (ctxt', xs) = foldl_map bind (ctxt, fixes);
     fun app t = foldl Term.betapply (t, xs);
-  in (fixes, map (apsnd (apsome app)) binds, map app assumes) end;
+  in (ctxt', (map (apsnd (apsome app)) binds, map app assumes)) end;
 
 fun pretty_cases (ctxt as Context {cases, ...}) =
   let
@@ -1036,9 +1036,9 @@
       | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s ::
             flat (Library.separate sep (map (Library.single o prt) xs))))];
 
-    fun prt_case (name, (xs, lets, asms)) = Pretty.block (Pretty.fbreaks
+    fun prt_case (name, (fixes, (lets, asms))) = Pretty.block (Pretty.fbreaks
       (Pretty.str (name ^ ":") ::
-        prt_sect "fix" [] (prt_term o Free) xs @
+        prt_sect "fix" [] (prt_term o Free) fixes @
         prt_sect "let" [Pretty.str "and"] prt_let
           (mapfilter (fn (xi, Some t) => Some (xi, t) | _ => None) lets) @
         prt_sect "assume" [] (Pretty.quote o prt_term) asms));
@@ -1046,7 +1046,8 @@
     val cases' = rev (Library.gen_distinct Library.eq_fst cases);
   in
     if null cases andalso not (! verbose) then []
-    else [Pretty.big_list "cases:" (map (prt_case o apsnd (apply_case ctxt)) cases')]
+    else [Pretty.big_list "cases:"
+      (map (prt_case o apsnd (fn c => (#fixes c, #2 (apply_case c ctxt)))) cases')]
   end;
 
 val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;

--- a/src/Pure/Isar/rule_cases.ML	Tue Jan 09 15:15:28 2001 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Tue Jan 09 15:17:08 2001 +0100
@@ -79,9 +79,7 @@
   let
     val (_, _, Bi, _) = Thm.dest_state (thm, i)
       handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
-    val xs =
-      (rev (rename_wrt_term Bi (Logic.strip_params Bi)))    (* FIXME avoid rename_wrt_term? *)
-      |> map (if open_parms then I else apfst Syntax.internal);
+    val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
     val concl_bind = ((case_conclN, 0),
       Some (Term.list_abs (xs, Logic.strip_assums_concl Bi)));