exported declare_names
authorhaftmann
Fri Dec 07 15:08:08 2007 +0100 (2007-12-07)
changeset 25573a0e695567236
parent 25572 0c9052719f20
child 25574 016f677ad7b8
exported declare_names
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Fri Dec 07 15:08:07 2007 +0100
     1.2 +++ b/src/Pure/variable.ML	Fri Dec 07 15:08:08 2007 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    val def_type: Proof.context -> bool -> indexname -> typ option
     1.5    val def_sort: Proof.context -> indexname -> sort option
     1.6    val declare_constraints: term -> Proof.context -> Proof.context
     1.7 +  val declare_names: term -> Proof.context -> Proof.context
     1.8    val declare_internal: term -> Proof.context -> Proof.context
     1.9    val declare_term: term -> Proof.context -> Proof.context
    1.10    val declare_prf: Proofterm.proof -> Proof.context -> Proof.context