New function read_cterms is a combination of read_def_cterm and
read_cterm. It reads and simultaneously type-checks a list of strings.
cterm_of no longer catches exception TYPE; instead it must be caught later on
and a message printed using Sign.exn_type_msg. More informative messages can
be printed this way.
(* Title: HOLCF/fun3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of => (fun) for class pcpo
*)
Fun3 = Fun2 +
(* default class is still term *)
arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *)
rules
inst_fun_pcpo "UU::'a=>'b::pcpo = UU_fun"
end