# HG changeset patch
# User boehmes
# Date 1289573767 -3600
# Node ID 1204d268464ffb529c15947b9a58f9cfd64f3624
# Parent  fd218201da5e29328783f33f8483f0b076d5c42a
look for certificates relative to the theory

diff -r fd218201da5e -r 1204d268464f src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -81,7 +81,7 @@
 
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
 
-declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
+declare [[smt_certificates="Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
 declare [[smt_oracle=false]]
 
diff -r fd218201da5e -r 1204d268464f src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -38,7 +38,7 @@
 
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
 
-declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
+declare [[smt_certificates="Boogie_Max.certs"]]
 declare [[smt_fixed=true]]
 declare [[smt_oracle=false]]
 
diff -r fd218201da5e -r 1204d268464f src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -46,7 +46,7 @@
 
 boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
 
-declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
+declare [[smt_certificates="VCC_Max.certs"]]
 declare [[smt_fixed=true]]
 declare [[smt_oracle=false]]
 
diff -r fd218201da5e -r 1204d268464f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -7,7 +7,7 @@
   imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
 begin
 
-declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
+declare [[smt_certificates="Integration.certs"]]
 declare [[smt_fixed=true]]
 declare [[smt_oracle=false]]
 
diff -r fd218201da5e -r 1204d268464f src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 declare [[smt_solver=z3, smt_oracle=false]]
-declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Examples.certs"]]
+declare [[smt_certificates="SMT_Examples.certs"]]
 declare [[smt_fixed=true]]
 
 
diff -r fd218201da5e -r 1204d268464f src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 declare [[smt_solver=z3, smt_oracle=false]]
-declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Tests.certs"]]
+declare [[smt_certificates="SMT_Tests.certs"]]
 declare [[smt_fixed=true]]
 
 
diff -r fd218201da5e -r 1204d268464f src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Nov 12 15:56:07 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 declare [[smt_solver=z3, smt_oracle=true]]
-declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Word_Examples.certs"]]
+declare [[smt_certificates="SMT_Word_Examples.certs"]]
 declare [[smt_fixed=true]]
 
 
diff -r fd218201da5e -r 1204d268464f src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Fri Nov 12 15:56:06 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Nov 12 15:56:07 2010 +0100
@@ -173,9 +173,12 @@
 val get_certificates_path =
   Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
 
-fun select_certificates name = Certificates.put (
+fun select_certificates name context = context |> Certificates.put (
   if name = "" then NONE
-  else SOME (Cache_IO.make (Path.explode name)))
+  else
+    Path.explode name
+    |> Path.append (Thy_Load.master_directory (Context.theory_of context))
+    |> SOME o Cache_IO.make)
 
 val certificates_of = Certificates.get o Context.Proof