1199 val (raw_ctxt, raw_proppss) = declare_elemss prep_parms fixed_params raw_elemss context; |
1199 val (raw_ctxt, raw_proppss) = declare_elemss prep_parms fixed_params raw_elemss context; |
1200 (* CB: raw_ctxt is context with additional fixed variables derived from |
1200 (* CB: raw_ctxt is context with additional fixed variables derived from |
1201 the fixes elements in raw_elemss, |
1201 the fixes elements in raw_elemss, |
1202 raw_proppss contains assumptions and definitions from the |
1202 raw_proppss contains assumptions and definitions from the |
1203 external elements in raw_elemss. *) |
1203 external elements in raw_elemss. *) |
1204 val raw_propps = map List.concat raw_proppss; |
1204 fun prep_prop raw_ctxt raw_concl raw_propp = |
1205 val raw_propp = List.concat raw_propps; |
1205 let |
1206 |
1206 (* CB: add type information from fixed_params to context (declare_term) *) |
1207 (* CB: add type information from fixed_params to context (declare_term) *) |
1207 (* CB: process patterns (conclusion and external elements only) *) |
1208 (* CB: process patterns (conclusion and external elements only) *) |
1208 val (ctxt, all_propp) = |
1209 val (ctxt, all_propp) = |
1209 prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); |
1210 prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); |
1210 (* CB: add type information from conclusion and external elements to context *) |
1211 (* CB: add type information from conclusion and external elements |
1211 val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt; |
1212 to context *) |
1212 (* CB: resolve schematic variables (patterns) in conclusion and external elements. *) |
1213 val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt; |
1213 val all_propp' = map2 (curry (op ~~)) |
1214 |
1214 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); |
1215 (* CB: resolve schematic variables (patterns) in conclusion and external |
1215 val (concl, propp) = splitAt (length raw_concl, all_propp') |
1216 elements. *) |
1216 in ((ctxt, concl), propp) end |
1217 val all_propp' = map2 (curry (op ~~)) |
1217 |
1218 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); |
1218 val ((ctxt, concl), proppss) = (burrow_split o burrow_split) (prep_prop raw_ctxt raw_concl) raw_proppss; |
1219 val (concl, propp) = splitAt(length raw_concl, all_propp'); |
|
1220 val propps = unflat raw_propps propp; |
|
1221 val proppss = map (uncurry unflat) (raw_proppss ~~ propps); |
|
1222 |
1219 |
1223 (* CB: obtain all parameters from identifier part of raw_elemss *) |
1220 (* CB: obtain all parameters from identifier part of raw_elemss *) |
1224 val xs = map #1 (params_of' raw_elemss); |
1221 val xs = map #1 (params_of' raw_elemss); |
1225 val typing = unify_frozen ctxt 0 |
1222 val typing = unify_frozen ctxt 0 |
1226 (map (ProofContext.default_type raw_ctxt) xs) |
1223 (map (ProofContext.default_type raw_ctxt) xs) |