# HG changeset patch
# User wenzelm
# Date 927280122 -7200
# Node ID acbcf8085166574f13f98ece04d5d9092c24ef19
# Parent  169e5b07ec06fa6050a7d4e2954decfc22929247
typedef_proof: pass interactive flag;

diff -r 169e5b07ec06 -r acbcf8085166 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri May 21 11:46:42 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri May 21 11:48:42 1999 +0200
@@ -15,8 +15,10 @@
     term -> string list -> thm list -> tactic option -> theory -> theory
   val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
     term -> string list -> thm list -> tactic option -> theory -> theory
-  val typedef_proof: string -> bstring * string list * mixfix -> string -> theory -> ProofHistory.T
-  val typedef_proof_i: string -> bstring * string list * mixfix -> term -> theory -> ProofHistory.T
+  val typedef_proof: string -> bstring * string list * mixfix -> string
+    -> bool -> theory -> ProofHistory.T
+  val typedef_proof_i: string -> bstring * string list * mixfix -> term
+    -> bool -> theory -> ProofHistory.T
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -187,13 +189,13 @@
 fun typedef_attribute cset do_typedef (thy, thm) =
   (check_nonempty cset thm; (thy |> do_typedef, thm));
 
-fun gen_typedef_proof prep_term name typ set thy =
+fun gen_typedef_proof prep_term name typ set int thy =
   let
     val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
     val goal = Thm.term_of (goal_nonempty cset);
   in
     thy
-    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, [])
+    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;