src/ZF/Tools/ind_cases.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18799 f137c5e971f5
     1.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -53,7 +53,7 @@
     1.4      val read_prop = ProofContext.read_prop (ProofContext.init thy);
     1.5      val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
     1.6      val facts = args |> map (fn ((name, srcs), props) =>
     1.7 -      ((name, map (Attrib.global_attribute thy) srcs),
     1.8 +      ((name, map (Attrib.attribute thy) srcs),
     1.9          map (Thm.no_attributes o single o mk_cases) props));
    1.10    in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
    1.11