src/Pure/facts.ML
changeset 29581 b3b33e0298eb
parent 29269 5c25a2012975
child 29848 a7c164e228e1
     1.1 --- a/src/Pure/facts.ML	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/src/Pure/facts.ML	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -30,9 +30,9 @@
     1.4    val props: T -> thm list
     1.5    val could_unify: T -> term -> thm list
     1.6    val merge: T * T -> T
     1.7 -  val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
     1.8 -  val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
     1.9 -  val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
    1.10 +  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
    1.11 +  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
    1.12 +  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
    1.13    val del: string -> T -> T
    1.14    val hide: bool -> string -> T -> T
    1.15  end;