src/Pure/Isar/rule_cases.ML

         chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
       in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
 
 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;
     val nested = is_some case_outline andalso len > 1;