equal
deleted
inserted
replaced
74 val thy = thy |> Theory.parent_path |
74 val thy = thy |> Theory.parent_path |
75 in |
75 in |
76 add_fundef_data name (fundef_data, mutual_info, spec) thy |
76 add_fundef_data name (fundef_data, mutual_info, spec) thy |
77 end |
77 end |
78 |
78 |
79 fun gen_add_fundef prep_att eqns_attss preprocess thy = |
79 fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy = |
80 let |
80 let |
81 fun prep_eqns neqs = |
81 fun prep_eqns neqs = |
82 neqs |
82 neqs |
83 |> map (apsnd (Sign.read_prop thy)) |
83 |> map (apsnd (Sign.read_prop thy)) |
84 |> map (apfst (apsnd (apfst (map (prep_att thy))))) |
84 |> map (apfst (apsnd (apfst (map (prep_att thy))))) |