src/Pure/Isar/code_unit.ML
changeset 25485 33840a854e63
parent 25336 027a63deb61c
child 25540 e209975d5606
equal deleted inserted replaced
25484:4c98517601ce 25485:33840a854e63
    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