src/HOL/Tools/typedef_package.ML
changeset 12004 1703de633aaf
parent 11968 859a141085d0
child 12043 8c86683597a8
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Oct 31 21:58:04 2001 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 31 21:59:07 2001 +0100
     1.3 @@ -244,7 +244,8 @@
     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 ((("", [att]), (goal, ([goal_pat], []))), comment) int
     1.8 +    thy |> IsarThy.theorem_i Drule.internalK None
     1.9 +      ((("", [att]), (goal, ([goal_pat], []))), comment) int
    1.10    end;
    1.11  
    1.12  val typedef_proof = gen_typedef_proof read_term;