- { K.proof_name = Some "name";
- K.proof_id = gen_id seed;
- K.proof_context = [];
- K.proof_apply_context = flat seed p;
- K.proof_conclude =
- { K.conclude_id = gen_id seed;
- K.conclude_aref = id;
- K.conclude_method = "Case";
- K.conclude_args = (K.Term ty)::(K.Term te)::pp;
- K.conclude_conclusion =
- try Some
- (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
- with Not_found -> None
- }
- }
- | None ->
- { K.proof_name = name;
- K.proof_id = gen_id seed;
- K.proof_context = [];
- K.proof_apply_context = [];
- K.proof_conclude =
- { K.conclude_id = gen_id seed;
- K.conclude_aref = id;
- K.conclude_method = "Case";
- K.conclude_args = (K.Term ty)::(K.Term te)::pp;
- K.conclude_conclusion =
- try Some
- (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
- with Not_found -> None
- }
- }
- )
+ (flat seed p,
+ K.Premise
+ { K.premise_id = gen_id seed;
+ K.premise_xref = p.K.proof_id;
+ K.premise_binder = p.K.proof_name;
+ K.premise_n = None
+ })
+ | None -> [],K.Term te) in
+ { K.proof_name = name;
+ K.proof_id = gen_id seed;
+ K.proof_context = [];
+ K.proof_apply_context = apply_context;
+ K.proof_conclude =
+ { K.conclude_id = gen_id seed;
+ K.conclude_aref = id;
+ K.conclude_method = "Case";
+ K.conclude_args =
+ (K.Aux (UriManager.string_of_uri uri))::
+ (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+ K.conclude_conclusion =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with Not_found -> None
+ }
+ }