# HG changeset patch
# User wenzelm
# Date 921185509 -3600
# Node ID b5f1f861155dba9f610a1955bfd269c9ade45f4b
# Parent  f7750d816c2158c745e6cf4e5fbff2a11d97134a
workaround default_name problem;

diff -r f7750d816c21 -r b5f1f861155d src/Pure/pure_thy.ML
--- 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;