# HG changeset patch
# User wenzelm
# Date 963481143 -7200
# Node ID c5875175751f79d077692e4fedc13974e953b5a7
# Parent  23705d14be8f6e3d15fa4287a550ebefcececa9f
invoke_case: bind_skolem;

diff -r 23705d14be8f -r c5875175751f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jul 13 11:38:42 2000 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 13 11:39:03 2000 +0200
@@ -524,10 +524,13 @@
 (* invoke_case *)
 
 fun invoke_case (name, atts) state =
-  let val (vars, props) = get_case state name in
+  let
+    val (vars, props) = get_case state name;
+    val bind_skolem = ProofContext.bind_skolem (context_of state) (map #1 vars);
+  in
     state
     |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
-    |> assume_i [(name, atts, map (fn t => (t, ([], []))) props)]
+    |> assume_i [(name, atts, map (fn t => (t, ([], []))) (map bind_skolem props))]
   end;
 
 
@@ -565,7 +568,7 @@
   in
     state'
     |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
-    |> map_context (ProofContext.add_cases (RuleCases.make goal [antN]))
+    |> map_context (ProofContext.add_cases (RuleCases.make false goal [antN]))
     |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block