equal
deleted
inserted
replaced
530 then () |
530 then () |
531 else out "const_maps" |
531 else out "const_maps" |
532 val _ = app (fn (hol,(internal,isa,opt_ty)) => |
532 val _ = app (fn (hol,(internal,isa,opt_ty)) => |
533 (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); |
533 (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); |
534 case opt_ty of |
534 case opt_ty of |
535 SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of thy ty)) ^ "\"") |
535 SOME ty => out (" :: \"" ^ (Display.string_of_ctyp (ctyp_of thy ty)) ^ "\"") |
536 | NONE => ())) constmaps |
536 | NONE => ())) constmaps |
537 val _ = if null constmaps |
537 val _ = if null constmaps |
538 then () |
538 then () |
539 else out "\n\n" |
539 else out "\n\n" |
540 |
540 |