src/ZF/Tools/ind_cases.ML
changeset 18418 bf448d999b7e
parent 17412 e26cb20ef0cc
child 18678 dd0c569fa43d
     1.1 --- a/src/ZF/Tools/ind_cases.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4      val facts = args |> map (fn ((name, srcs), props) =>
     1.5        ((name, map (Attrib.global_attribute thy) srcs),
     1.6          map (Thm.no_attributes o single o mk_cases) props));
     1.7 -  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
     1.8 +  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
     1.9  
    1.10  
    1.11  (* ind_cases method *)