src/HOL/Tools/typedef_package.ML
changeset 12043 8c86683597a8
parent 12004 1703de633aaf
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Sun Nov 04 20:56:19 2001 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sun Nov 04 20:56:59 2001 +0100
     1.3 @@ -244,7 +244,7 @@
     1.4        prepare_typedef prep_term true name typ set opt_morphs thy;
     1.5      val att = #1 o att_result;
     1.6    in
     1.7 -    thy |> IsarThy.theorem_i Drule.internalK None
     1.8 +    thy |> IsarThy.theorem_i Drule.internalK (None, [])
     1.9        ((("", [att]), (goal, ([goal_pat], []))), comment) int
    1.10    end;
    1.11