adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Renamed symtab storing tvar information.

This commit is contained in:
Achim D. Brucker 2018-06-24 21:06:06 +01:00
parent 479c60b2f3
commit e53d1bcb01
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Hiding_Type_Variables.thy
View File

@ -101,14 +101,14 @@ structure Hide_Tvar : HIDE_TVAR = struct
}
type hide_tvar_tab = (hide_varT) Symtab.table
fun hide_tvar_eq (a, a') = (#name a) = (#name a')
fun merge_assert_tab (tab,tab') = Symtab.merge hide_tvar_eq (tab,tab')
fun merge_tvar_tab (tab,tab') = Symtab.merge hide_tvar_eq (tab,tab')
structure Data = Generic_Data
(
type T = hide_tvar_tab
val empty = Symtab.empty:hide_tvar_tab
val extend = I
fun merge(t1,t2) = merge_assert_tab (t1, t2)
fun merge(t1,t2) = merge_tvar_tab (t1, t2)
);