1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Oct 22 14:15:43 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 22 14:15:44 2008 +0200
     1.3 @@ -2097,7 +2097,7 @@
     1.4              val tnames = map fst tfrees
     1.5              val tsyn = mk_syn thy tycname
     1.6              val typ = (tycname,tnames,tsyn)
     1.7 -            val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
     1.8 +            val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy
     1.9              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
    1.10  
    1.11              val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
    1.12 @@ -2183,7 +2183,7 @@
    1.13              val tnames = sort string_ord (map fst tfrees)
    1.14              val tsyn = mk_syn thy tycname
    1.15              val typ = (tycname,tnames,tsyn)
    1.16 -            val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    1.17 +            val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    1.18              val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
    1.19              val fulltyname = Sign.intern_type thy' tycname
    1.20              val aty = Type (fulltyname, map mk_vartype tnames)

     2.1 --- a/src/HOL/Import/replay.ML	Wed Oct 22 14:15:43 2008 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Wed Oct 22 14:15:44 2008 +0200
     2.3 @@ -344,7 +344,7 @@
     2.4  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
     2.5  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
     2.6  	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
     2.7 -	    snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     2.8 +	    snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     2.9  	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    2.10  	    add_hol4_type_mapping thyname tycname true fulltyname thy
    2.11  	  | delta (Indexed_theorem (i, th)) thy = 

     3.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Oct 22 14:15:43 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Oct 22 14:15:44 2008 +0200
     3.3 @@ -608,7 +608,7 @@
     3.4      val (typedefs, thy6) =
     3.5        thy4
     3.6        |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
     3.7 -          TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx)
     3.8 +          TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
     3.9              (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    3.10                 Const (cname, U --> HOLogic.boolT)) NONE
    3.11              (rtac exI 1 THEN rtac CollectI 1 THEN

     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 22 14:15:43 2008 +0200
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 22 14:15:44 2008 +0200
     4.3 @@ -194,7 +194,7 @@
     4.4      val (typedefs, thy3) = thy2 |>
     4.5        parent_path flat_names |>
     4.6        fold_map (fn ((((name, mx), tvs), c), name') =>
     4.7 -          TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx)
     4.8 +          TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
     4.9              (Collect $ Const (c, UnivT')) NONE
    4.10              (rtac exI 1 THEN rtac CollectI 1 THEN
    4.11                QUIET_BREADTH_FIRST (has_fewer_prems 1)

     5.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Oct 22 14:15:43 2008 +0200
     5.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 22 14:15:44 2008 +0200
     5.3 @@ -15,12 +15,10 @@
     5.4      Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
     5.5    val get_info: theory -> string -> info option
     5.6    val add_typedef: bool -> string option -> bstring * string list * mixfix ->
     5.7 -    string -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
     5.8 -  val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
     5.9      term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
    5.10 -  val typedef: (bool * string) * (bstring * string list * mixfix) * string
    5.11 +  val typedef: (bool * string) * (bstring * string list * mixfix) * term
    5.12      * (string * string) option -> theory -> Proof.state
    5.13 -  val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    5.14 +  val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
    5.15      * (string * string) option -> theory -> Proof.state
    5.16    val interpretation: (string -> theory -> theory) -> theory -> theory
    5.17    val setup: theory -> theory
    5.18 @@ -33,15 +31,15 @@
    5.19  
    5.20  val type_definitionN = "Typedef.type_definition";
    5.21  
    5.22 -val Rep = thm "type_definition.Rep";
    5.23 -val Rep_inverse = thm "type_definition.Rep_inverse";
    5.24 -val Abs_inverse = thm "type_definition.Abs_inverse";
    5.25 -val Rep_inject = thm "type_definition.Rep_inject";
    5.26 -val Abs_inject = thm "type_definition.Abs_inject";
    5.27 -val Rep_cases = thm "type_definition.Rep_cases";
    5.28 -val Abs_cases = thm "type_definition.Abs_cases";
    5.29 -val Rep_induct = thm "type_definition.Rep_induct";
    5.30 -val Abs_induct = thm "type_definition.Abs_induct";
    5.31 +val Rep = @{thm "type_definition.Rep"};
    5.32 +val Rep_inverse = @{thm "type_definition.Rep_inverse"};
    5.33 +val Abs_inverse = @{thm "type_definition.Abs_inverse"};
    5.34 +val Rep_inject = @{thm "type_definition.Rep_inject"};
    5.35 +val Abs_inject = @{thm "type_definition.Abs_inject"};
    5.36 +val Rep_cases = @{thm "type_definition.Rep_cases"};
    5.37 +val Abs_cases = @{thm "type_definition.Abs_cases"};
    5.38 +val Rep_induct = @{thm "type_definition.Rep_induct"};
    5.39 +val Abs_induct = @{thm "type_definition.Abs_induct"};
    5.40  
    5.41  
    5.42  
    5.43 @@ -214,27 +212,18 @@
    5.44    handle ERROR msg => err_in_typedef msg name;
    5.45  
    5.46  
    5.47 -(* add_typedef interfaces *)
    5.48 +(* add_typedef interface *)
    5.49  
    5.50 -local
    5.51 -
    5.52 -fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
    5.53 +fun add_typedef def opt_name typ set opt_morphs tac thy =
    5.54    let
    5.55      val name = the_default (#1 typ) opt_name;
    5.56      val (set, goal, _, typedef_result) =
    5.57 -      prepare_typedef prep_term def name typ set opt_morphs thy;
    5.58 +      prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
    5.59      val non_empty = Goal.prove_global thy [] [] goal (K tac)
    5.60        handle ERROR msg => cat_error msg
    5.61          ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
    5.62    in typedef_result non_empty thy end;
    5.63  
    5.64 -in
    5.65 -
    5.66 -val add_typedef = gen_typedef Syntax.read_term;
    5.67 -val add_typedef_i = gen_typedef Syntax.check_term;
    5.68 -
    5.69 -end;
    5.70 -
    5.71  
    5.72  (* Isar typedef interface *)
    5.73  
    5.74 @@ -249,8 +238,8 @@
    5.75  
    5.76  in
    5.77  
    5.78 -val typedef = gen_typedef Syntax.read_term;
    5.79 -val typedef_i = gen_typedef Syntax.check_term;
    5.80 +val typedef = gen_typedef Syntax.check_term;
    5.81 +val typedef_cmd = gen_typedef Syntax.read_term;
    5.82  
    5.83  end;
    5.84  
    5.85 @@ -270,7 +259,7 @@
    5.86      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    5.87  
    5.88  fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    5.89 -  typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
    5.90 +  typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
    5.91  
    5.92  val _ =
    5.93    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal

     6.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Oct 22 14:15:43 2008 +0200
     6.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Wed Oct 22 14:15:44 2008 +0200
     6.3 @@ -89,7 +89,7 @@
     6.4      fun make_po tac thy1 =
     6.5        let
     6.6          val ((_, {type_definition, set_def, ...}), thy2) = thy1
     6.7 -          |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac;
     6.8 +          |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
     6.9          val lthy3 = thy2
    6.10            |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
    6.11          val less_def' = Syntax.check_term lthy3 less_def;