equal
deleted
inserted
replaced
2448 Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro)) |
2448 Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro)) |
2449 "adding alternative introduction rules for code generation of inductive predicates" |
2449 "adding alternative introduction rules for code generation of inductive predicates" |
2450 (*FIXME name discrepancy in attribs and ML code*) |
2450 (*FIXME name discrepancy in attribs and ML code*) |
2451 (*FIXME intros should be better named intro*) |
2451 (*FIXME intros should be better named intro*) |
2452 |
2452 |
2453 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *) |
2453 (* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *) |
2454 fun generic_code_pred prep_const options raw_const lthy = |
2454 fun generic_code_pred prep_const options raw_const lthy = |
2455 let |
2455 let |
2456 val thy = ProofContext.theory_of lthy |
2456 val thy = ProofContext.theory_of lthy |
2457 val const = prep_const thy raw_const |
2457 val const = prep_const thy raw_const |
2458 val lthy' = LocalTheory.theory (PredData.map |
2458 val lthy' = LocalTheory.theory (PredData.map |