Relax on type agreement with original context when applying term syntax.

--- a/src/FOL/ex/LocaleTest.thy	Sat Oct 17 23:07:53 2009 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Mon Nov 02 21:27:26 2009 +0100
@@ -124,6 +124,57 @@
 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 {*
+if Display.string_of_thm @{context} @{thm d1_def} <>
+ "\^E\^Fterm\^E\^E\^Fconst\^Fname=local.d1\^Ed1\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Ffixed\^Fname=p1\^E\^E\^Ffree\^Ep1\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E))\^E\^F\^E" 
+then error "Theorem syntax 'd1(?x) <-> ~ p2(p1(?x))' expected." else ();
+if Display.string_of_thm @{context} @{thm d2_def} <>
+ "\^E\^Fterm\^E\^E\^Fconst\^Fname=local.d2\^Ed2\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E)\^E\^F\^E"
+then error "Theorem syntax 'd2(?x) <-> ~ p2(?x)' expected." else ();
+*}
+
+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 {*
+if Display.string_of_thm @{context} @{thm d1_def} <>
+ "\^E\^Fterm\^E\^E\^Fconst\^Fname=LocaleTest.syntax.d1\^Esyntax.d1\^E\^F\^E(\^E\^Ffixed\^Fname=p3\^E\^E\^Ffree\^Ep3\^E\^F\^E\^E\^F\^E, \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E, \^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Ffixed\^Fname=p3\^E\^E\^Ffree\^Ep3\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E))\^E\^F\^E"
+then error "Theorem syntax 'syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))' expected."
+else ();
+if Display.string_of_thm @{context} @{thm d2_def} <>
+ "\^E\^Fterm\^E\^E\^Fconst\^Fname=local.d2\^Ed2\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E)\^E\^F\^E"
+then error "Theorem syntax 'd2(?x) <-> ~ p2(?x)' expected." else ();
+*}
+
+end
+
+
 section {* Foundational versions of theorems *}
 
 thm logic.assoc

--- a/src/Pure/Isar/theory_target.ML	Sat Oct 17 23:07:53 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Nov 02 21:27:26 2009 +0100
@@ -178,7 +178,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 = Binding.eq_name (b, b')