# HG changeset patch
# User haftmann
# Date 1253542296 -7200
# Node ID 827cac8abeccb65b991e7842b52f3efac1f08cbf
# Parent  72b93132fc3124a1918c7727d1ada5e57a53f6f3# Parent  55a0be42327c5c281ba9acc2aa0a7bb9dbddae66
merged

diff -r 55a0be42327c -r 827cac8abecc src/HOL/SMT/IsaMakefile
--- a/src/HOL/SMT/IsaMakefile	Mon Sep 21 16:01:38 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-## targets
-
-default: HOL-SMT
-images: HOL-SMT
-test: 
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-USEDIR = $(ISATOOL) usedir -v true 
-
-
-## HOL-SMT
-
-HOL-SMT: $(OUT)/HOL-SMT
-
-$(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \
-  Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \
-  Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \
-  Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \
-  Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \
-  Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML
-	@$(USEDIR) -b HOL-Word HOL-SMT
-
-$(OUT)/HOL-Word:
-	@$(ISATOOL) make HOL-Word -C $(SRC)/HOL
-
-
-## clean
-
-clean:
-	@rm -f $(OUT)/HOL-SMT
diff -r 55a0be42327c -r 827cac8abecc src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 16:01:38 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Mon Sep 21 16:11:36 2009 +0200
@@ -55,8 +55,6 @@
 
 exception SMT_COUNTEREXAMPLE of bool * term list
 
-val theory_of = Context.cases I ProofContext.theory_of
-
 
 datatype interface = Interface of {
   normalize: SMT_Normalize.config list,
@@ -177,12 +175,12 @@
 val solver_name_of = snd o SelectedSolver.get
 
 fun select_solver name gen =
-  if is_none (lookup_solver (theory_of gen) name)
+  if is_none (lookup_solver (Context.theory_of gen) name)
   then error ("SMT solver not registered: " ^ quote name)
   else SelectedSolver.map (K (serial (), name)) gen
 
 fun raw_solver_of gen =
-  (case lookup_solver (theory_of gen) (solver_name_of gen) of
+  (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
     NONE => error "No SMT solver selected"
   | SOME (s, _) => s)
 
@@ -228,11 +226,11 @@
 fun print_setup gen =
   let
     val t = string_of_int (Config.get_generic gen timeout)
-    val names = sort string_ord (all_solver_names_of (theory_of gen))
+    val names = sort string_ord (all_solver_names_of (Context.theory_of gen))
     val ns = if null names then [no_solver] else names
     val take_info = (fn (_, []) => NONE | info => SOME info)
     val infos =
-      theory_of gen
+      Context.theory_of gen
       |> Symtab.dest o Solvers.get
       |> map_filter (fn (n, (_, info)) => take_info (n, info gen))
       |> sort (prod_ord string_ord (K EQUAL))
diff -r 55a0be42327c -r 827cac8abecc src/HOL/SMT/lib/scripts/remote_smt.pl