equal
deleted
inserted
replaced
124 |
124 |
125 fun extern_term syntax = |
125 fun extern_term syntax = |
126 let |
126 let |
127 val (structs, fixes) = idents_of syntax; |
127 val (structs, fixes) = idents_of syntax; |
128 fun map_free (t as Free (x, T)) = |
128 fun map_free (t as Free (x, T)) = |
129 let val i = Library.find_index_eq x structs + 1 in |
129 let val i = find_index (fn s => s = x) structs + 1 in |
130 if i = 0 andalso member (op =) fixes x then |
130 if i = 0 andalso member (op =) fixes x then |
131 Const (Syntax.fixedN ^ x, T) |
131 Const (Syntax.fixedN ^ x, T) |
132 else if i = 1 andalso not (! show_structs) then |
132 else if i = 1 andalso not (! show_structs) then |
133 Syntax.const "_struct" $ Syntax.const "_indexdefault" |
133 Syntax.const "_struct" $ Syntax.const "_indexdefault" |
134 else t |
134 else t |