src/ZF/Tools/ind_cases.ML

--- a/src/ZF/Tools/ind_cases.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -55,7 +55,7 @@
     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));
-  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
+  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
 
 
 (* ind_cases method *)