# HG changeset patch
# User haftmann
# Date 1197036488 -3600
# Node ID a0e695567236132364ff732033bb8351a1afbb82
# Parent  0c9052719f20c8b25ebbaf09abf3eb9ca3b6efad
exported declare_names

diff -r 0c9052719f20 -r a0e695567236 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Dec 07 15:08:07 2007 +0100
+++ b/src/Pure/variable.ML	Fri Dec 07 15:08:08 2007 +0100
@@ -23,6 +23,7 @@
   val def_type: Proof.context -> bool -> indexname -> typ option
   val def_sort: Proof.context -> indexname -> sort option
   val declare_constraints: term -> Proof.context -> Proof.context
+  val declare_names: term -> Proof.context -> Proof.context
   val declare_internal: term -> Proof.context -> Proof.context
   val declare_term: term -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context