equal
deleted
inserted
replaced
108 let |
108 let |
109 val fmap' = map Library.swap fmap |
109 val fmap' = map Library.swap fmap |
110 fun unthaw (f as (a,S)) = |
110 fun unthaw (f as (a,S)) = |
111 (case assoc (fmap',a) of |
111 (case assoc (fmap',a) of |
112 NONE => TVar f |
112 NONE => TVar f |
113 | SOME b => TFree (b,S)) |
113 | SOME (b, _) => TFree (b,S)) |
114 in |
114 in |
115 map_term_types (map_type_tvar unthaw) t |
115 map_term_types (map_type_tvar unthaw) t |
116 end |
116 end |
117 |
117 |
118 (* The syntactic meddling needed to setup add_specification for work *) |
118 (* The syntactic meddling needed to setup add_specification for work *) |