src/HOL/Tools/typedef_package.ML
changeset 11740 86ac4189a1c1
parent 11727 a27150cc8fa5
child 11744 3a4625eaead0
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Oct 13 20:31:05 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 13 20:31:34 2001 +0200
     1.3 @@ -216,8 +216,10 @@
     1.4  (* typedef_proof interface *)
     1.5  
     1.6  fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
     1.7 -  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy;
     1.8 -  in thy |> IsarThy.theorem_i ((("", [att]), (goal, ([goal_pat], []))), comment) int end;
     1.9 +  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy in
    1.10 +    thy
    1.11 +    |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
    1.12 +  end;
    1.13  
    1.14  val typedef_proof = gen_typedef_proof read_term;
    1.15  val typedef_proof_i = gen_typedef_proof cert_term;