workaround default_name problem;

--- a/src/Pure/pure_thy.ML	Thu Mar 11 13:20:35 1999 +0100
+++ b/src/Pure/pure_thy.ML	Thu Mar 11 21:51:49 1999 +0100
@@ -221,7 +221,7 @@
 
 fun enter_thmx sg app_name (bname, thmx) =
   let
-    val name = Sign.full_name sg bname;
+    val name = Sign.full_name sg (default_name bname);
     val named_thms = map Thm.name_thm (app_name name thmx);
 
     val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;