# HG changeset patch
# User wenzelm
# Date 1125237891 -7200
# Node ID 7667a85b53f11833bcebc6eeda4abb2a6a81448c
# Parent  dc3b8cec8bba2d234d874d247245bb6edce6b6ee
unskolem local vars;

diff -r dc3b8cec8bba -r 7667a85b53f1 src/Pure/Isar/rule_cases.ML
--- 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