135 fn thy => |
135 fn thy => |
136 let |
136 let |
137 val thyname = get_import_thy thy |
137 val thyname = get_import_thy thy |
138 in |
138 in |
139 Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy |
139 Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy |
140 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Sign.read_typ thy ty) thy) (thy,constmaps) |
140 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps) |
141 end) |
141 end) |
142 |
142 |
143 val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) |
143 val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) |
144 >> (fn constmaps => |
144 >> (fn constmaps => |
145 fn thy => |
145 fn thy => |
146 let |
146 let |
147 val thyname = get_import_thy thy |
147 val thyname = get_import_thy thy |
148 in |
148 in |
149 Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy |
149 Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy |
150 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Sign.read_typ thy ty) thy) (thy,constmaps) |
150 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps) |
151 end) |
151 end) |
152 |
152 |
153 fun import_thy s = |
153 fun import_thy s = |
154 let |
154 let |
155 val is = TextIO.openIn(s ^ ".imp") |
155 val is = TextIO.openIn(s ^ ".imp") |