unskolem local vars;

--- a/src/Pure/Isar/rule_cases.ML	Sun Aug 28 16:04:50 2005 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Sun Aug 28 16:04:51 2005 +0200
@@ -94,11 +94,14 @@
   assumes: (string * term list) list,
   binds: (indexname * term option) list};
 
+fun unskolem x =
+  (case try Syntax.dest_skolem x of SOME x' => x' | NONE => x);
+
 fun prep_case is_open sg (split, raw_prop) name =
   let
     val prop = Drule.norm_hhf sg raw_prop;
 
-    val xs = Logic.strip_params prop;
+    val xs = map (apfst unskolem) (Logic.strip_params prop);
     val rename = if is_open then I else map (apfst Syntax.internal);
     val named_xs =
       (case split of