changeset 18799 | f137c5e971f5 |
parent 18728 | 6790126ab5f6 |
child 18928 | 042608ffa2ec |
--- a/src/HOL/Tools/typedef_package.ML Fri Jan 27 18:29:33 2006 +0100 +++ b/src/HOL/Tools/typedef_package.ML Fri Jan 27 19:03:02 2006 +0100 @@ -256,7 +256,7 @@ val (_, goal, goal_pat, att_result) = prepare_typedef prep_term def name typ set opt_morphs thy; val att = #1 o att_result; - in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([goal_pat], [])) thy end; + in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end; in