equal
deleted
inserted
replaced
648 then () |
648 then () |
649 else out "const_maps" |
649 else out "const_maps" |
650 val _ = app (fn (hol,(internal,isa,opt_ty)) => |
650 val _ = app (fn (hol,(internal,isa,opt_ty)) => |
651 (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); |
651 (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); |
652 case opt_ty of |
652 case opt_ty of |
653 Some ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"") |
653 Some ty => out (" :: \"" ^ (Output.output (string_of_ctyp (ctyp_of sg ty))) ^ "\"") |
654 | None => ())) constmaps |
654 | None => ())) constmaps |
655 val _ = if null constmaps |
655 val _ = if null constmaps |
656 then () |
656 then () |
657 else out "\n\n" |
657 else out "\n\n" |
658 |
658 |