equal
deleted
inserted
replaced
57 fun warning_thm f thm = SOME (f thm) handle BAD_THM msg |
57 fun warning_thm f thm = SOME (f thm) handle BAD_THM msg |
58 => (warning ("code generator: " ^ msg); NONE); |
58 => (warning ("code generator: " ^ msg); NONE); |
59 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; |
59 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; |
60 |
60 |
61 fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy); |
61 fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy); |
62 fun string_of_const thy c = case Class.param_const thy c |
62 fun string_of_const thy c = case Class.inst_of_param thy c |
63 of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) |
63 of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) |
64 | NONE => Sign.extern_const thy c; |
64 | NONE => Sign.extern_const thy c; |
65 |
65 |
66 fun no_args thy = length o fst o strip_type o Sign.the_const_type thy; |
66 fun no_args thy = length o fst o strip_type o Sign.the_const_type thy; |
67 |
67 |