# HG changeset patch
# User boehmes
# Date 1257496040 -3600
# Node ID 8c489493e65ea68d4681463e5f7b484d3ae6a72a
# Parent  c047b522b6cec293e363e234ac2c4f9c1b421fbf
tuned

diff -r c047b522b6ce -r 8c489493e65e src/HOL/Boogie/Boogie.thy
--- a/src/HOL/Boogie/Boogie.thy	Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/Boogie/Boogie.thy	Fri Nov 06 09:27:20 2009 +0100
@@ -193,8 +193,8 @@
 structure Boogie_Axioms = Named_Thms
 (
   val name = "boogie"
-  val description = ("Boogie background axioms" ^
-    " loaded along with Boogie verification conditions")
+  val description =
+    "Boogie background axioms loaded along with Boogie verification conditions"
 )
 *}
 setup Boogie_Axioms.setup
@@ -207,8 +207,8 @@
 structure Split_VC_SMT_Rules = Named_Thms
 (
   val name = "split_vc_smt"
-  val description = ("Theorems given to the SMT sub-tactic" ^
-    " of the split_vc method")
+  val description =
+    "theorems given to the SMT sub-tactic of the split_vc method"
 )
 *}
 setup Split_VC_SMT_Rules.setup
diff -r c047b522b6ce -r 8c489493e65e src/HOL/Boogie/Examples/ROOT.ML
--- a/src/HOL/Boogie/Examples/ROOT.ML	Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/Boogie/Examples/ROOT.ML	Fri Nov 06 09:27:20 2009 +0100
@@ -1,3 +1,1 @@
-use_thy "Boogie_Max";
-use_thy "Boogie_Dijkstra";
-use_thy "VCC_Max";
+use_thys ["Boogie_Max", "Boogie_Dijkstra", "VCC_Max"];
diff -r c047b522b6ce -r 8c489493e65e src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 06 09:27:20 2009 +0100
@@ -136,13 +136,11 @@
     in get_first is_builtin end
 
   fun lookup_const thy name T =
-    let
-      val intern = Sign.intern_const thy name
-      val is_type_instance = Type.typ_instance o Sign.tsig_of
+    let val intern = Sign.intern_const thy name
     in
       if Sign.declared_const thy intern
       then
-        if is_type_instance thy (T, Sign.the_const_type thy intern)
+        if Sign.typ_instance thy (T, Sign.the_const_type thy intern)
         then SOME (Const (intern, T))
         else error ("Boogie: function already declared with different type: " ^
           quote name)
diff -r c047b522b6ce -r 8c489493e65e src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Nov 05 20:42:47 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 09:27:20 2009 +0100
@@ -5,7 +5,7 @@
 header {* Examples for the 'smt' tactic. *}
 
 theory SMT_Examples
-imports "../SMT"
+imports SMT
 begin
 
 declare [[smt_solver=z3, z3_proofs=true]]