src/HOL/Tools/typedef_package.ML
changeset 6690 acbcf8085166
parent 6383 45bb139e6ceb
child 6723 f342449d73ca
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri May 21 11:46:42 1999 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri May 21 11:48:42 1999 +0200
     1.3 @@ -15,8 +15,10 @@
     1.4      term -> string list -> thm list -> tactic option -> theory -> theory
     1.5    val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
     1.6      term -> string list -> thm list -> tactic option -> theory -> theory
     1.7 -  val typedef_proof: string -> bstring * string list * mixfix -> string -> theory -> ProofHistory.T
     1.8 -  val typedef_proof_i: string -> bstring * string list * mixfix -> term -> theory -> ProofHistory.T
     1.9 +  val typedef_proof: string -> bstring * string list * mixfix -> string
    1.10 +    -> bool -> theory -> ProofHistory.T
    1.11 +  val typedef_proof_i: string -> bstring * string list * mixfix -> term
    1.12 +    -> bool -> theory -> ProofHistory.T
    1.13  end;
    1.14  
    1.15  structure TypedefPackage: TYPEDEF_PACKAGE =
    1.16 @@ -187,13 +189,13 @@
    1.17  fun typedef_attribute cset do_typedef (thy, thm) =
    1.18    (check_nonempty cset thm; (thy |> do_typedef, thm));
    1.19  
    1.20 -fun gen_typedef_proof prep_term name typ set thy =
    1.21 +fun gen_typedef_proof prep_term name typ set int thy =
    1.22    let
    1.23      val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
    1.24      val goal = Thm.term_of (goal_nonempty cset);
    1.25    in
    1.26      thy
    1.27 -    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, [])
    1.28 +    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) int
    1.29    end;
    1.30  
    1.31  val typedef_proof = gen_typedef_proof read_term;