1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Oct 12 12:06:23 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Oct 12 12:06:54 2001 +0200
     1.3 @@ -147,9 +147,9 @@
     1.4        |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
     1.5         [Logic.mk_defpair (setC, set)])
     1.6        |> PureThy.add_axioms_i [((typedef_name, typedef_prop),
     1.7 -          [apsnd (fn cond_axm => standard (nonempty RS cond_axm))])]
     1.8 +          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
     1.9        |> (fn (theory', axm) =>
    1.10 -        let fun make th = standard (th OF axm) in
    1.11 +        let fun make th = Drule.standard (th OF axm) in
    1.12            rpair (hd axm) (theory'
    1.13            |> (#1 oo PureThy.add_thms)
    1.14              ([((Rep_name, make Rep), []),
    1.15 @@ -193,8 +193,8 @@
    1.16  
    1.17      (*test theory errors now!*)
    1.18      val test_thy = Theory.copy thy;
    1.19 -    val test_sign = Theory.sign_of test_thy;
    1.20 -    val _ = (test_thy, Thm.assume (Thm.cterm_of test_sign goal)) |> typedef_att;
    1.21 +    val _ = (test_thy,
    1.22 +      setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_att;
    1.23  
    1.24    in (cset, goal, goal_pat, typedef_att) end
    1.25    handle ERROR => err_in_typedef name;