# HG changeset patch
# User blanchet
# Date 1380551334 -7200
# Node ID ba9254f3111bc753f42bcfa448764a68d1bc5f38
# Parent  b352d3d4a58a928720c362490b2dc71058487017
added possibility to reset builtins (for experimentation)

diff -r b352d3d4a58a -r ba9254f3111b src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Sep 30 16:07:56 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Mon Sep 30 16:28:54 2013 +0200
@@ -6,6 +6,9 @@
 
 signature SMT_BUILTIN =
 sig
+  (*for experiments*)
+  val clear_builtins: Proof.context -> Proof.context
+
   (*built-in types*)
   val add_builtin_typ: SMT_Utils.class ->
     typ * (typ -> string option) * (typ -> int -> string option) ->
@@ -105,6 +108,9 @@
   fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
 )
 
+val clear_builtins = Context.proof_map (Builtins.put ([], Symtab.empty))
+
+
 (* built-in types *)
 
 fun add_builtin_typ cs (T, f, g) =
@@ -196,7 +202,7 @@
   special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
 
 fun dest_builtin ctxt c ts =
-  let val t =Term.list_comb (Const c, ts)
+  let val t = Term.list_comb (Const c, ts)
   in
     (case dest_builtin_num ctxt t of
       SOME (n, _) => SOME (n, 0, [], K t)