merged

--- a/src/FOL/ex/LocaleTest.thy	Thu Nov 05 23:59:23 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Fri Nov 06 10:26:13 2009 +0100
@@ -124,6 +124,59 @@
 thm var.test_def
 
 
+text {* Under which circumstances term syntax remains active. *}
+
+locale "syntax" =
+  fixes p1 :: "'a => 'b"
+    and p2 :: "'b => o"
+begin
+
+definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
+definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
+
+thm d1_def d2_def
+
+end
+
+thm syntax.d1_def syntax.d2_def
+
+locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
+begin
+
+thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
+
+ML {*
+  fun check_syntax ctxt thm expected =
+    let
+      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
+    in
+      if obtained <> expected
+      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
+      else ()
+    end;
+*}
+
+ML {*
+  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+*}
+
+end
+
+locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
+begin
+
+thm d1_def d2_def
+  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
+
+ML {*
+  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+*}
+
+end
+
+
 section {* Foundational versions of theorems *}
 
 thm logic.assoc

--- a/src/HOL/Boogie/Boogie.thy	Thu Nov 05 23:59:23 2009 +0100
+++ b/src/HOL/Boogie/Boogie.thy	Fri Nov 06 10:26:13 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

--- a/src/HOL/Boogie/Examples/ROOT.ML	Thu Nov 05 23:59:23 2009 +0100
+++ b/src/HOL/Boogie/Examples/ROOT.ML	Fri Nov 06 10:26:13 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"];

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Nov 05 23:59:23 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 06 10:26:13 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)

--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Nov 05 23:59:23 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 10:26:13 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]]

--- a/src/Pure/Isar/theory_target.ML	Thu Nov 05 23:59:23 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 06 10:26:13 2009 +0100
@@ -190,7 +190,9 @@
     val b' = Morphism.binding phi b;
     val rhs' = Morphism.term phi rhs;
     val arg = (b', Term.close_schematic_term rhs');
-    val similar_body = Type.similar_types (rhs, rhs');
+(*    val similar_body = Type.similar_types (rhs, rhs'); *)
+    val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
+    val similar_body = same_shape (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
     val class_global =