diff -r b790ce4c21c2 -r a1d8806b5267 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sun Dec 10 15:30:43 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sun Dec 10 15:30:44 2006 +0100
@@ -91,7 +91,7 @@
 
 fun extract_case is_open thy (case_outline, raw_prop) name concls =
   let
-    val rename = if is_open then I else (apfst Name.internal);
+    val rename = if is_open then I else (apfst (Name.internal o Name.clean));
 
     val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
     val len = length props;