# HG changeset patch
# User wenzelm
# Date 1165761044 -3600
# Node ID a1d8806b5267938877ad903d4a45994c86c3c283
# Parent  b790ce4c21c205ceeee56a2ac878b6b9e7bdd2d8
extract_case: Name.clean;

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;