src/HOL/Tools/datatype_package.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26496 49ae9456eba9
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -391,7 +391,7 @@
     1.4    | ManyConstrs (thm, simpset) =>
     1.5        let
     1.6          val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
     1.7 -          map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
     1.8 +          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
     1.9              ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
    1.10        in
    1.11          Goal.prove (Simplifier.the_context ss) [] [] eq_t (K