added chop_prefix

class_of_param instead of class_of

adaptions in class_package

adaptions in codegen

variants: special treatment of empty name;

avoid reference to internal skolem;

separate names filed (covers fixes/defaults);

adapted Name.defaults_of;

removed obsolete xless; tuned zero_var_indexes;

clean: no special treatment of empty name; declare, invent: clean arguments;

removed obsolete xless;

replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes

uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;

replaced read_radixint by read_intinf;

removed str_to_int in favour of general Syntax.read_xnum;

num/xnum: bin or hex;

Name.internal; Name.invent_list;

tuned;

* Pure: structure Name;

Names of basic logical entities (variables etc.).

replaced Term.variant(list) by Name.variant(_list); removed obsolete mem_term;

Name.internal; Name.dest_skolem;

adapted to more efficient Name/Variable implementation; removed dead code;

replaced Term.variant(list) by Name.variant(_list); Name.internal;

maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML);

removed obsolete mem_ix;

removed obsolete ins_ix, mem_ix, ins_term, mem_term; moved variant(list), invent_names, bound, dest_internal/skolem etc. to name.ML;

Name.dest_skolem;

Name.bound;

replaced Term.variant(list) by Name.variant(_list); Name.bound;