exported declare_names
authorhaftmann
Fri, 07 Dec 2007 15:08:08 +0100
changeset 25573 a0e695567236
parent 25572 0c9052719f20
child 25574 016f677ad7b8
exported declare_names
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