- Tried to make name_of_thm more robust against changes of the structure of proofs. - Now uses add_inductive_global rather than add_inductive_i for the definition of the realizability predicate.

- Removed occurrences of ProofContext.export in add_ind_def that caused theorems to end up in the wrong context - Explicit parameters are now generalized in theorems returned by add_inductive(_i)

thy_deps: sort Context.thy_ord;

added thy_ord -- order of creation; ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);