Tests enforce proper export behaviour.

--- a/src/FOL/ex/LocaleTest.thy	Mon Nov 05 15:37:41 2007 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Mon Nov 05 17:47:52 2007 +0100
@@ -52,12 +52,13 @@
 locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
   assumes hom: "h(x ** y) = h(x) ++ h(y)"
 
-(*
-FIXME: graceful handling of type errors?
+
+(* FIXME: graceful handling of type errors?
 locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
   assumes "mult(x) == add"
 *)
 
+
 locale LV = LU _ add
 
 locale LW = LU _ mult (infixl "**" 60)
@@ -156,11 +157,6 @@
 print_interps IC  (* output: <no prefix, i1 *)
 print_interps ID  (* output: i2, i3 *)
 
-(* schematic vars in instantiation not permitted *)
-(*
-interpretation i4: IA ["?x::?'a1"] apply (rule IA.intro) apply rule done
-print_interps IA
-*)
 
 interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
 
@@ -189,17 +185,19 @@
 
 locale IF = fixes f assumes asm_F: "f & f --> f"
 
+consts default :: "'a"
+
 theorem True
 proof -
-  fix alpha::i and beta and gamma::o
-  have alpha_A: "IA(alpha)" by unfold_locales simp
+  fix alpha::i and beta
+  have alpha_A: "IA(alpha)" by unfold_locales
   interpret i5: IA [alpha] .  (* subsumed *)
   print_interps IA  (* output: <no prefix>, i1 *)
   interpret i6: IC [alpha beta] by unfold_locales auto
   print_interps IA   (* output: <no prefix>, i1 *)
   print_interps IC   (* output: <no prefix>, i1, i6 *)
-  interpret i11: IF [gamma] by (fast intro: IF.intro)
-  thm i11.asm_F      (* gamma is a Free *)
+  interpret i11: IF ["default = default"] by (fast intro: IF.intro)
+  thm i11.asm_F [where 'a = i]     (* default has schematic type *)
 qed rule
 
 theorem (in IA) True
@@ -209,7 +207,6 @@
   interpret i9: ID [a beta _]
     apply - apply assumption
     apply unfold_locales
-    apply (rule refl) (*FIXME: should have been discharged by unfold_locales*)
     apply (rule refl) done
 qed rule