src/HOL/Tools/SMT/smt_datatypes.ML
changeset 57213 9daec42f6784
parent 43385 9cd4b4ecb4dd
child 57226 c22ad39c3b4b
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
     1.3 @@ -71,16 +71,18 @@
     1.4  
     1.5  (* typedef declarations *)
     1.6  
     1.7 -fun get_typedef_decl (info : Typedef.info) T Ts =
     1.8 -  let
     1.9 -    val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info
    1.10 +fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
    1.11 +    : Typedef.info) T Ts =
    1.12 +  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
    1.13 +    let
    1.14 +      val env = snd (Term.dest_Type abs_type) ~~ Ts
    1.15 +      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    1.16  
    1.17 -    val env = snd (Term.dest_Type abs_type) ~~ Ts
    1.18 -    val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    1.19 -
    1.20 -    val constr = Const (Abs_name, instT (rep_type --> abs_type))
    1.21 -    val select = Const (Rep_name, instT (abs_type --> rep_type))
    1.22 -  in (T, [(constr, [select])]) end
    1.23 +      val constr = Const (Abs_name, instT (rep_type --> abs_type))
    1.24 +      val select = Const (Rep_name, instT (abs_type --> rep_type))
    1.25 +    in [(T, [(constr, [select])])] end
    1.26 +  else
    1.27 +    []
    1.28  
    1.29  
    1.30  (* collection of declarations *)
    1.31 @@ -99,7 +101,7 @@
    1.32          | NONE =>
    1.33              (case Typedef.get_info ctxt n of
    1.34                [] => ([], ctxt)
    1.35 -            | info :: _ => ([get_typedef_decl info T Ts], ctxt))))
    1.36 +            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
    1.37    end
    1.38  
    1.39  fun add_decls T (declss, ctxt) =