1.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Sep 30 16:07:56 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Mon Sep 30 16:28:54 2013 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  signature SMT_BUILTIN =
     1.6  sig
     1.7 +  (*for experiments*)
     1.8 +  val clear_builtins: Proof.context -> Proof.context
     1.9 +
    1.10    (*built-in types*)
    1.11    val add_builtin_typ: SMT_Utils.class ->
    1.12      typ * (typ -> string option) * (typ -> int -> string option) ->
    1.13 @@ -105,6 +108,9 @@
    1.14    fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
    1.15  )
    1.16  
    1.17 +val clear_builtins = Context.proof_map (Builtins.put ([], Symtab.empty))
    1.18 +
    1.19 +
    1.20  (* built-in types *)
    1.21  
    1.22  fun add_builtin_typ cs (T, f, g) =
    1.23 @@ -196,7 +202,7 @@
    1.24    special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
    1.25  
    1.26  fun dest_builtin ctxt c ts =
    1.27 -  let val t =Term.list_comb (Const c, ts)
    1.28 +  let val t = Term.list_comb (Const c, ts)
    1.29    in
    1.30      (case dest_builtin_num ctxt t of
    1.31        SOME (n, _) => SOME (n, 0, [], K t)