src/Pure/Isar/local_theory.ML
changeset 24554 e9edafca311c
parent 24031 e94e541346d7
child 24933 5471b164813b
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Sep 07 17:56:03 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Sep 07 20:40:08 2007 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     1.5      local_theory -> (term * (bstring * thm)) * local_theory
     1.6    val note: string -> (bstring * Attrib.src list) * thm list ->
     1.7 -    local_theory -> (bstring * thm list) * Proof.context
     1.8 +    local_theory -> (bstring * thm list) * local_theory
     1.9    val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.10    val target_morphism: local_theory -> morphism
    1.11    val target_naming: local_theory -> NameSpace.naming