equal
deleted
inserted
replaced
1046 |
1046 |
1047 (* importing introduction rules *) |
1047 (* importing introduction rules *) |
1048 |
1048 |
1049 fun import_intros inp_pred [] ctxt = |
1049 fun import_intros inp_pred [] ctxt = |
1050 let |
1050 let |
1051 val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt |
1051 val (outp_pred, ctxt') = yield_singleton (Variable.import_terms true) inp_pred ctxt |
1052 val T = fastype_of outp_pred |
1052 val T = fastype_of outp_pred |
1053 val paramTs = ho_argsT_of_typ (binder_types T) |
1053 val paramTs = ho_argsT_of_typ (binder_types T) |
1054 val (param_names, _) = Variable.variant_fixes |
1054 val (param_names, _) = Variable.variant_fixes |
1055 (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt' |
1055 (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt' |
1056 val params = map2 (curry Free) param_names paramTs |
1056 val params = map2 (curry Free) param_names paramTs |