--- 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 *)
--- 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
--- 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;