equal
deleted
inserted
replaced
79 struct |
79 struct |
80 |
80 |
81 (** local context data **) |
81 (** local context data **) |
82 |
82 |
83 type fixes = string Name_Space.table; |
83 type fixes = string Name_Space.table; |
84 val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; |
84 val empty_fixes: fixes = Name_Space.empty_table Isabelle_Markup.fixedN; |
85 |
85 |
86 datatype data = Data of |
86 datatype data = Data of |
87 {is_body: bool, (*inner body mode*) |
87 {is_body: bool, (*inner body mode*) |
88 names: Name.context, (*type/term variable names*) |
88 names: Name.context, (*type/term variable names*) |
89 consts: string Symtab.table, (*consts within the local scope*) |
89 consts: string Symtab.table, (*consts within the local scope*) |