111 >> (fn constmaps => |
111 >> (fn constmaps => |
112 fn thy => |
112 fn thy => |
113 let |
113 let |
114 val thyname = get_import_thy thy |
114 val thyname = get_import_thy thy |
115 in |
115 in |
116 foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol false isa thy |
116 foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy |
117 | (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps) |
117 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps) |
118 end) |
118 end) |
119 |
119 |
120 val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) |
120 val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) |
121 >> (fn constmaps => |
121 >> (fn constmaps => |
122 fn thy => |
122 fn thy => |
123 let |
123 let |
124 val thyname = get_import_thy thy |
124 val thyname = get_import_thy thy |
125 in |
125 in |
126 foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol true isa thy |
126 foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy |
127 | (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps) |
127 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps) |
128 end) |
128 end) |
129 |
129 |
130 fun import_thy s = |
130 fun import_thy s = |
131 let |
131 let |
132 val is = TextIO.openIn(s ^ ".imp") |
132 val is = TextIO.openIn(s ^ ".imp") |
158 fun create_int_thms thyname thy = |
158 fun create_int_thms thyname thy = |
159 if !SkipProof.quick_and_dirty |
159 if !SkipProof.quick_and_dirty |
160 then thy |
160 then thy |
161 else |
161 else |
162 case ImportData.get thy of |
162 case ImportData.get thy of |
163 None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy |
163 NONE => ImportData.put (SOME (fst (Replay.setup_int_thms thyname thy))) thy |
164 | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?" |
164 | SOME _ => error "Import data not closed - forgotten an end_setup, mayhap?" |
165 |
165 |
166 fun clear_int_thms thy = |
166 fun clear_int_thms thy = |
167 if !SkipProof.quick_and_dirty |
167 if !SkipProof.quick_and_dirty |
168 then thy |
168 then thy |
169 else |
169 else |
170 case ImportData.get thy of |
170 case ImportData.get thy of |
171 None => error "Import data already cleared - forgotten a setup_theory?" |
171 NONE => error "Import data already cleared - forgotten a setup_theory?" |
172 | Some _ => ImportData.put None thy |
172 | SOME _ => ImportData.put NONE thy |
173 |
173 |
174 val setup_theory = P.name |
174 val setup_theory = P.name |
175 >> |
175 >> |
176 (fn thyname => |
176 (fn thyname => |
177 fn thy => |
177 fn thy => |