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