src/HOL/Tools/function_package/fundef_package.ML
changeset 20285 23f5cd23c1e1
parent 20270 3abe7dae681e
child 20320 a5368278a72c
equal deleted inserted replaced
20284:a17c737c82df 20285:23f5cd23c1e1
    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)))))