src/HOL/Tools/SMT/smt_datatypes.ML
changeset 58360 dee1fd1cc631
parent 58061 3d060f43accb
child 58361 7f2b3b6f6ad1
     1.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 16:20:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 16:53:39 2014 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature SMT_DATATYPES =
     1.6  sig
     1.7 -  val add_decls: typ ->
     1.8 +  val add_decls: BNF_Util.fp_kind -> typ ->
     1.9      (typ * (term * term list) list) list list * Proof.context ->
    1.10      (typ * (term * term list) list) list list * Proof.context
    1.11  end;
    1.12 @@ -63,7 +63,7 @@
    1.13          [] => ([], ctxt)
    1.14        | info :: _ => (get_typedef_decl info T Ts, ctxt)))
    1.15  
    1.16 -fun add_decls T (declss, ctxt) =
    1.17 +fun add_decls fp T (declss, ctxt) =
    1.18    let
    1.19      fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
    1.20