export read_typ/cert_typ -- version with regular context operations;
authorwenzelm
Thu Jun 19 20:48:01 2008 +0200 (2008-06-19)
changeset 272777b7ce2d7fafe
parent 27276 ea82bd1e3c20
child 27278 129574589734
export read_typ/cert_typ -- version with regular context operations;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Jun 19 20:48:00 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Jun 19 20:48:01 2008 +0200
     1.3 @@ -24,6 +24,8 @@
     1.4    val make_case :  Proof.context -> bool -> string list -> term ->
     1.5      (term * term) list -> term * (term * (int * bool)) list
     1.6    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
     1.7 +  val read_typ: theory ->
     1.8 +    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
     1.9    val interpretation : (string list -> theory -> theory) -> theory -> theory
    1.10    val rep_datatype : ({distinct : thm list list,
    1.11         inject : thm list list,
    1.12 @@ -304,17 +306,18 @@
    1.13  
    1.14  (* prepare types *)
    1.15  
    1.16 -fun read_typ sign ((Ts, sorts), str) =
    1.17 +fun read_typ thy ((Ts, sorts), str) =
    1.18    let
    1.19 -    val T = Type.no_tvars (Sign.read_def_typ (sign, AList.lookup (op =)
    1.20 -      (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
    1.21 -  in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
    1.22 +    val ctxt = ProofContext.init thy
    1.23 +      |> fold (Variable.declare_typ o TFree) sorts;
    1.24 +    val T = Syntax.read_typ ctxt str;
    1.25 +  in (Ts @ [T], Term.add_tfreesT T sorts) end;
    1.26  
    1.27  fun cert_typ sign ((Ts, sorts), raw_T) =
    1.28    let
    1.29      val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
    1.30        TYPE (msg, _, _) => error msg;
    1.31 -    val sorts' = add_typ_tfrees (T, sorts)
    1.32 +    val sorts' = Term.add_tfreesT T sorts;
    1.33    in (Ts @ [T],
    1.34        case duplicates (op =) (map fst sorts') of
    1.35           [] => sorts'