src/HOL/Tools/SMT/smt_translate.ML
changeset 58360 dee1fd1cc631
parent 58061 3d060f43accb
child 58361 7f2b3b6f6ad1
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 17 16:20:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 17 16:53:39 2014 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4      funcs: (string * (string list * string)) list }
     1.5    type config = {
     1.6      logic: term list -> string,
     1.7 -    has_datatypes: bool,
     1.8 +    fp_kinds: BNF_Util.fp_kind list,
     1.9      serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    1.10    type replay_data = {
    1.11      context: Proof.context,
    1.12 @@ -66,7 +66,7 @@
    1.13  
    1.14  type config = {
    1.15    logic: term list -> string,
    1.16 -  has_datatypes: bool,
    1.17 +  fp_kinds: BNF_Util.fp_kind list,
    1.18    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    1.19  
    1.20  type replay_data = {
    1.21 @@ -139,7 +139,8 @@
    1.22  
    1.23  fun collect_datatypes_and_records (tr_context, ctxt) ts =
    1.24    let
    1.25 -    val (declss, ctxt') = fold (Term.fold_types SMT_Datatypes.add_decls) ts ([], ctxt)
    1.26 +    val (declss, ctxt') =
    1.27 +      fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts ([], ctxt)
    1.28  
    1.29      fun is_decl_typ T = exists (exists (equal T o fst)) declss
    1.30  
    1.31 @@ -478,7 +479,7 @@
    1.32  
    1.33  fun translate ctxt smt_options comments ithms =
    1.34    let
    1.35 -    val {logic, has_datatypes, serialize} = get_config ctxt
    1.36 +    val {logic, fp_kinds, serialize} = get_config ctxt
    1.37  
    1.38      fun no_dtyps (tr_context, ctxt) ts =
    1.39        ((Termtab.empty, [], tr_context, ctxt), ts)
    1.40 @@ -487,7 +488,8 @@
    1.41  
    1.42      val ((funcs, dtyps, tr_context, ctxt1), ts2) =
    1.43        ((empty_tr_context, ctxt), ts1)
    1.44 -      |-> (if has_datatypes then collect_datatypes_and_records else no_dtyps)
    1.45 +      |-> (if member (op =) fp_kinds BNF_Util.Least_FP then collect_datatypes_and_records
    1.46 +        else no_dtyps)
    1.47  
    1.48      fun is_binder (Const (@{const_name Let}, _) $ _) = true
    1.49        | is_binder t = Lambda_Lifting.is_quantifier t