# HG changeset patch
# User wenzelm
# Date 1236250733 -3600
# Node ID 84097bba7bdc923f9a6174b28f9828485987a50e
# Parent  18ce07e05a957ddc0b6f1812af4bba9d13c9a59d
eliminated obsolete ProofContext.full_bname;

diff -r 18ce07e05a95 -r 84097bba7bdc src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Mar 05 10:54:03 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Mar 05 11:58:53 2009 +0100
@@ -114,7 +114,7 @@
 
 fun print_calculation false _ _ = ()
   | print_calculation true ctxt calc = Pretty.writeln
-      (ProofContext.pretty_fact ctxt (ProofContext.full_bname ctxt calculationN, calc));
+      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc));
 
 
 (* also and finally *)
diff -r 18ce07e05a95 -r 84097bba7bdc src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 05 10:54:03 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Mar 05 11:58:53 2009 +0100
@@ -1006,7 +1006,7 @@
     fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
     fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
     val after_qed' = (after_local', after_global');
-    val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN;
+    val this_name = ProofContext.full_name goal_ctxt (Binding.name AutoBind.thisN);
 
     val result_ctxt =
       state
diff -r 18ce07e05a95 -r 84097bba7bdc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 05 10:54:03 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 05 11:58:53 2009 +0100
@@ -23,7 +23,6 @@
   val set_stmt: bool -> Proof.context -> Proof.context
   val naming_of: Proof.context -> NameSpace.naming
   val full_name: Proof.context -> binding -> string
-  val full_bname: Proof.context -> bstring -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
@@ -243,9 +242,7 @@
   map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
 
 val naming_of = #naming o rep_context;
-
 val full_name = NameSpace.full_name o naming_of;
-fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
 
 val syntax_of = #syntax o rep_context;
 val syn_of = LocalSyntax.syn_of o syntax_of;