src/ZF/Tools/ind_cases.ML

 fun inductive_cases args thy =
   let
     val read_prop = ProofContext.read_prop (ProofContext.init thy);
     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
     val facts = args |> map (fn ((name, srcs), props) =>
-      (((name, map (Attrib.global_attribute thy) srcs),
-        map (Thm.no_attributes o single o mk_cases) props), Comment.none));
+      ((name, map (Attrib.global_attribute thy) srcs),
+        map (Thm.no_attributes o single o mk_cases) props));
   in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
 
 
 (* ind_cases method *)
 

 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val ind_cases =
-  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment)
+  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
   >> (Toplevel.theory o inductive_cases);
 
 val inductive_casesP =
   OuterSyntax.command "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;