diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -99,7 +99,7 @@
   apply (rule L_nat)
   done
 
-interpretation L: M_trivial L by (rule M_trivial_L)
+interpretation L?: M_trivial L by (rule M_trivial_L)
 
 (* Replaces the following declarations...
 lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]