src/Pure/more_thm.ML

--- a/src/Pure/more_thm.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/more_thm.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -281,7 +281,7 @@
   let
     val name' = if name = "" then "axiom_" ^ serial_string () else name;
     val thy' = thy |> Theory.add_axioms_i [(name', prop)];
-    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' name'));
+    val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name'));
   in (axm, thy') end;
 
 fun add_def unchecked overloaded (name, prop) thy =
@@ -293,7 +293,7 @@
 
     val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
     val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
-    val axm' = Thm.axiom thy' (Sign.full_name thy' name);
+    val axm' = Thm.axiom thy' (Sign.full_bname thy' name);
     val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   in (thm, thy') end;