equal
deleted
inserted
replaced
72 val extra_size = Option.map fst o BNF_LFP_Size.lookup_size_global thy; |
72 val extra_size = Option.map fst o BNF_LFP_Size.lookup_size_global thy; |
73 |
73 |
74 val (((size_names, size_fns), def_names), def_names') = |
74 val (((size_names, size_fns), def_names), def_names') = |
75 recTs1 |> map (fn T as Type (s, _) => |
75 recTs1 |> map (fn T as Type (s, _) => |
76 let |
76 let |
77 val s' = Long_Name.base_name s ^ "_size"; |
77 val s' = "size_" ^ Long_Name.base_name s; |
78 val s'' = Sign.full_bname thy s'; |
78 val s'' = Sign.full_bname thy s'; |
79 in |
79 in |
80 (s'', |
80 (s'', |
81 (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT), |
81 (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT), |
82 map snd param_size_fs), |
82 map snd param_size_fs), |