stripped some legacy bindings

--- a/src/HOL/Auth/Public.thy	Fri Dec 01 16:08:45 2006 +0100
+++ b/src/HOL/Auth/Public.thy	Fri Dec 01 17:22:28 2006 +0100
@@ -402,15 +402,14 @@
        insert_Key_singleton 
        Key_not_used insert_Key_image Un_assoc [THEN sym]
 
-ML
-{*
+ML {*
 val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
 val analz_image_freshK_simps = thms "analz_image_freshK_simps";
+val imp_disjL = thm "imp_disjL";
 
-val analz_image_freshK_ss = 
-     simpset() delsimps [image_insert, image_Un]
-	       delsimps [imp_disjL]    (*reduces blow-up*)
-	       addsimps thms "analz_image_freshK_simps"
+val analz_image_freshK_ss = simpset() delsimps [image_insert, image_Un]
+  delsimps [imp_disjL]    (*reduces blow-up*)
+  addsimps thms "analz_image_freshK_simps"
 *}
 
 method_setup analz_freshK = {*

--- a/src/HOL/HOL.ML	Fri Dec 01 16:08:45 2006 +0100
+++ b/src/HOL/HOL.ML	Fri Dec 01 17:22:28 2006 +0100
@@ -20,7 +20,6 @@
 
 val split_tac        = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
-val split_asm_tac    = Splitter.split_asm_tac;
 
 val op addsplits     = Splitter.addsplits;
 val op delsplits     = Splitter.delsplits;
@@ -38,175 +37,100 @@
 open BasicClassical;
 open Clasimp;
 
-val eq_reflection = thm "eq_reflection";
-val def_imp_eq = thm "def_imp_eq";
-val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
-val ccontr = thm "ccontr";
-val impI = thm "impI";
-val impCE = thm "impCE";
-val notI = thm "notI";
-val notE = thm "notE";
-val iffI = thm "iffI";
-val iffCE = thm "iffCE";
-val conjI = thm "conjI";
-val conjE = thm "conjE";
-val disjCI = thm "disjCI";
-val disjE = thm "disjE";
-val TrueI = thm "TrueI";
-val FalseE = thm "FalseE";
-val allI = thm "allI";
+val all_conj_distrib = thm "all_conj_distrib";
+val all_dupE = thm "all_dupE"
 val allE = thm "allE";
-val exI = thm "exI";
-val exE = thm "exE";
-val ex_ex1I = thm "ex_ex1I";
-val the_equality = thm "the_equality";
-val mp = thm "mp";
-val rev_mp = thm "rev_mp"
+val allI = thm "allI";
+val all_simps = thms "all_simps";
+val arg_cong = thm "arg_cong";
+val atomize_not = thm "atomize_not";
+val box_equals = thm "box_equals"
+val case_split = thm "case_split_thm";
+val case_split_thm = thm "case_split_thm"
+val cases_simp = thm "cases_simp";
+val ccontr = thm "ccontr";
+val choice_eq = thm "choice_eq"
 val classical = thm "classical";
-val subst = thm "subst";
-val refl = thm "refl";
-val sym = thm "sym";
-val trans = thm "trans";
-val arg_cong = thm "arg_cong";
-val iffD1 = thm "iffD1";
-val iffD2 = thm "iffD2";
-val disjE = thm "disjE";
+val cong = thm "cong"
+val conj_comms = thms "conj_comms";
+val conj_cong = thm "conj_cong";
+val conjE = thm "conjE"
 val conjE = thm "conjE";
-val exE = thm "exE";
-val contrapos_nn = thm "contrapos_nn";
-val contrapos_pp = thm "contrapos_pp";
-val notnotD = thm "notnotD";
+val conjI = thm "conjI";
 val conjunct1 = thm "conjunct1";
 val conjunct2 = thm "conjunct2";
-val spec = thm "spec";
-val imp_cong = thm "imp_cong";
-val the_sym_eq_trivial = thm "the_sym_eq_trivial";
-val triv_forall_equality = thm "triv_forall_equality";
-val case_split = thm "case_split_thm";
-val ext = thm "ext"
-val True_def = thm "True_def"
-val All_def = thm "All_def"
-val Ex_def = thm "Ex_def"
-val False_def = thm "False_def"
-val not_def = thm "not_def"
-val and_def = thm "and_def"
-val or_def = thm "or_def"
-val Ex1_def = thm "Ex1_def"
-val iff = thm "iff"
-val True_or_False = thm "True_or_False"
-val Let_def = thm "Let_def"
-val if_def = thm "if_def"
-val ssubst = thm "ssubst"
-val box_equals = thm "box_equals"
-val fun_cong = thm "fun_cong"
-val cong = thm "cong"
-val rev_iffD2 = thm "rev_iffD2"
-val rev_iffD1 = thm "rev_iffD1"
-val iffE = thm "iffE"
-val eqTrueI = thm "eqTrueI"
-val eqTrueE = thm "eqTrueE"
-val all_dupE = thm "all_dupE"
-val FalseE = thm "FalseE"
-val False_neq_True = thm "False_neq_True"
-val False_not_True = thm "False_not_True"
-val True_not_False = thm "True_not_False"
-val notI2 = thm "notI2"
-val impE = thm "impE"
-val not_sym = thm "not_sym"
-val rev_contrapos = thm "rev_contrapos"
-val conjE = thm "conjE"
-val context_conjI = thm "context_conjI"
-val disjI1 = thm "disjI1"
-val disjI2 = thm "disjI2"
-val rev_notE = thm "rev_notE"
-val ex1I = thm "ex1I"
-val ex1E = thm "ex1E"
-val ex1_implies_ex = thm "ex1_implies_ex"
-val the_equality = thm "the_equality"
-val theI = thm "theI"
-val theI' = thm "theI'"
-val theI2 = thm "theI2"
-val the1_equality = thm "the1_equality"
-val excluded_middle = thm "excluded_middle"
-val case_split_thm = thm "case_split_thm"
-val exCI = thm "exCI"
-val choice_eq = thm "choice_eq"
-val eq_cong2 = thm "eq_cong2"
-val if_cong = thm "if_cong"
-val if_weak_cong = thm "if_weak_cong"
-val let_weak_cong = thm "let_weak_cong"
-val eq_cong2 = thm "eq_cong2"
-val if_distrib = thm "if_distrib"
-val restrict_to_left = thm "restrict_to_left"
-val all_conj_distrib = thm "all_conj_distrib";
-val atomize_not = thm "atomize_not";
-val split_if = thm "split_if";
-val split_if_asm = thm "split_if_asm";
-val rev_conj_cong = thm "rev_conj_cong";
-val not_all = thm "not_all";
-val not_ex = thm "not_ex";
-val not_iff = thm "not_iff";
-val not_imp = thm "not_imp";
-val not_not = thm "not_not";
-val eta_contract_eq = thm "eta_contract_eq";
-val eq_ac = thms "eq_ac";
-val eq_commute = thm "eq_commute";
-val eq_sym_conv = thm "eq_commute";
-val neq_commute = thm "neq_commute";
-val conj_comms = thms "conj_comms";
-val conj_commute = thm "conj_commute";
-val conj_cong = thm "conj_cong";
-val conj_disj_distribL = thm "conj_disj_distribL";
-val conj_disj_distribR = thm "conj_disj_distribR";
-val conj_left_commute = thm "conj_left_commute";
-val disj_comms = thms "disj_comms";
-val disj_commute = thm "disj_commute";
-val disj_cong = thm "disj_cong";
-val disj_conj_distribL = thm "disj_conj_distribL";
-val disj_conj_distribR = thm "disj_conj_distribR";
-val disj_left_commute = thm "disj_left_commute";
-val eq_assoc = thm "eq_assoc";
-val eq_left_commute = thm "eq_left_commute";
-val ex_disj_distrib = thm "ex_disj_distrib";
-val if_P = thm "if_P";
-val if_bool_eq_disj = thm "if_bool_eq_disj";
-val if_def2 = thm "if_bool_eq_conj";
-val if_not_P = thm "if_not_P";
-val if_splits = thms "if_splits";
-val imp_all = thm "imp_all";
-val imp_conjL = thm "imp_conjL";
-val imp_conjR = thm "imp_conjR";
-val imp_disj_not1 = thm "imp_disj_not1";
-val imp_disj_not2 = thm "imp_disj_not2";
-val imp_ex = thm "imp_ex";
-val meta_eq_to_obj_eq = thm "def_imp_eq";
-val ex_simps = thms "ex_simps";
-val all_simps = thms "all_simps";
-val simp_thms = thms "simp_thms";
-val Eq_FalseI = thm "Eq_FalseI";
-val Eq_TrueI = thm "Eq_TrueI";
-val cases_simp = thm "cases_simp";
-val conj_assoc = thm "conj_assoc";
+val def_imp_eq = thm "def_imp_eq";
 val de_Morgan_conj = thm "de_Morgan_conj";
 val de_Morgan_disj = thm "de_Morgan_disj";
 val disj_assoc = thm "disj_assoc";
-val disj_not1 = thm "disj_not1";
-val disj_not2 = thm "disj_not2";
-val if_False = thm "if_False";
-val if_True = thm "if_True";
-val if_bool_eq_conj = thm "if_bool_eq_conj";
+val disjCI = thm "disjCI";
+val disj_comms = thms "disj_comms";
+val disj_cong = thm "disj_cong";
+val disjE = thm "disjE";
+val disjI1 = thm "disjI1"
+val disjI2 = thm "disjI2"
+val eq_ac = thms "eq_ac";
+val eq_cong2 = thm "eq_cong2"
+val Eq_FalseI = thm "Eq_FalseI";
+val eq_reflection = thm "eq_reflection";
+val Eq_TrueI = thm "Eq_TrueI";
+val Ex1_def = thm "Ex1_def"
+val ex1E = thm "ex1E"
+val ex1_implies_ex = thm "ex1_implies_ex"
+val ex1I = thm "ex1I"
+val excluded_middle = thm "excluded_middle"
+val ex_disj_distrib = thm "ex_disj_distrib";
+val exE = thm "exE";
+val exI = thm "exI";
+val ex_simps = thms "ex_simps";
+val ext = thm "ext"
+val FalseE = thm "FalseE"
+val FalseE = thm "FalseE";
+val fun_cong = thm "fun_cong"
 val if_cancel = thm "if_cancel";
 val if_eq_cancel = thm "if_eq_cancel";
+val if_False = thm "if_False";
 val iff_conv_conj_imp = thm "iff_conv_conj_imp";
+val iffD1 = thm "iffD1";
+val iffD2 = thm "iffD2";
+val iffI = thm "iffI";
+val iff = thm "iff"
+val if_splits = thms "if_splits";
+val if_True = thm "if_True";
+val if_weak_cong = thm "if_weak_cong"
+val imp_all = thm "imp_all";
 val imp_cong = thm "imp_cong";
+val imp_conjL = thm "imp_conjL";
+val imp_conjR = thm "imp_conjR";
 val imp_conv_disj = thm "imp_conv_disj";
-val imp_disj1 = thm "imp_disj1";
-val imp_disj2 = thm "imp_disj2";
-val imp_disjL = thm "imp_disjL";
-val simp_impliesI = thm "simp_impliesI";
-val simp_implies_cong = thm "simp_implies_cong";
+val impE = thm "impE"
+val impI = thm "impI";
+val Let_def = thm "Let_def"
+val meta_eq_to_obj_eq = thm "def_imp_eq";
+val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
+val mp = thm "mp";
+val not_all = thm "not_all";
+val notE = thm "notE";
+val not_ex = thm "not_ex";
+val not_iff = thm "not_iff";
+val notI = thm "notI";
+val not_not = thm "not_not";
+val not_sym = thm "not_sym"
+val refl = thm "refl";
+val rev_mp = thm "rev_mp"
 val simp_implies_def = thm "simp_implies_def";
+val simp_thms = thms "simp_thms";
+val spec = thm "spec";
+val split_if = thm "split_if";
+val ssubst = thm "ssubst"
+val subst = thm "subst";
+val sym = thm "sym";
+val the1_equality = thm "the1_equality"
+val theI = thm "theI"
+val theI' = thm "theI'"
+val trans = thm "trans";
 val True_implies_equals = thm "True_implies_equals";
+val TrueI = thm "TrueI";
 
 structure HOL =
 struct

--- a/src/HOL/Lattices.thy	Fri Dec 01 16:08:45 2006 +0100
+++ b/src/HOL/Lattices.thy	Fri Dec 01 17:22:28 2006 +0100
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
 *)
 
-header {* Lattices via Locales *}
+header {* Abstract lattices *}
 
 theory Lattices
 imports Orderings
@@ -187,29 +187,4 @@
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
                mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
 
-text {* ML legacy bindings *}
-
-ML {*
-val Least_def = thm "Least_def";
-val Least_equality = thm "Least_equality";
-val min_def = thm "min_def";
-val min_of_mono = thm "min_of_mono";
-val max_def = thm "max_def";
-val max_of_mono = thm "max_of_mono";
-val min_leastL = thm "min_leastL";
-val max_leastL = thm "max_leastL";
-val min_leastR = thm "min_leastR";
-val max_leastR = thm "max_leastR";
-val le_max_iff_disj = thm "le_max_iff_disj";
-val le_maxI1 = thm "le_maxI1";
-val le_maxI2 = thm "le_maxI2";
-val less_max_iff_disj = thm "less_max_iff_disj";
-val max_less_iff_conj = thm "max_less_iff_conj";
-val min_less_iff_conj = thm "min_less_iff_conj";
-val min_le_iff_disj = thm "min_le_iff_disj";
-val min_less_iff_disj = thm "min_less_iff_disj";
-val split_min = thm "split_min";
-val split_max = thm "split_max";
-*}
-
 end

--- a/src/HOL/Orderings.ML	Fri Dec 01 16:08:45 2006 +0100
+++ b/src/HOL/Orderings.ML	Fri Dec 01 17:22:28 2006 +0100
@@ -1,21 +1,6 @@
 (* legacy ML bindings *)
 
-val order_eq_refl = thm "order_eq_refl";
 val order_less_irrefl = thm "order_less_irrefl";
-val order_le_less = thm "order_le_less";
-val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
-val order_less_imp_le = thm "order_less_imp_le";
-val order_less_not_sym = thm "order_less_not_sym";
-val order_less_asym = thm "order_less_asym";
-val order_less_trans = thm "order_less_trans";
-val order_le_less_trans = thm "order_le_less_trans";
-val order_less_le_trans = thm "order_less_le_trans";
-val order_less_imp_not_less = thm "order_less_imp_not_less";
-val order_less_imp_triv = thm "order_less_imp_triv";
-val order_less_imp_not_eq = thm "order_less_imp_not_eq";
-val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
-val linorder_less_linear = thm "linorder_less_linear";
-val linorder_cases = thm "linorder_cases";
 val linorder_not_less = thm "linorder_not_less";
 val linorder_not_le = thm "linorder_not_le";
 val linorder_neq_iff = thm "linorder_neq_iff";
@@ -23,8 +8,10 @@
 val order_refl = thm "order_refl";
 val order_trans = thm "order_trans";
 val order_antisym = thm "order_antisym";
-val order_less_le = thm "order_less_le";
-val linorder_linear = thm "linorder_linear";
 val mono_def = thm "mono_def";
 val monoI = thm "monoI";
 val monoD = thm "monoD";
+val max_less_iff_conj = thm "max_less_iff_conj";
+val min_less_iff_conj = thm "min_less_iff_conj";
+val split_min = thm "split_min";
+val split_max = thm "split_max";

--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Dec 01 16:08:45 2006 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Dec 01 17:22:28 2006 +0100
@@ -104,6 +104,7 @@
 text{*This ML code does the inductions directly.*}
 ML{*
 val ns_constrainsI = thm "ns_constrainsI";
+val impCE = thm "impCE";
 
 fun ns_constrains_tac(cs,ss) i =
    SELECT_GOAL

--- a/src/HOLCF/domain/theorems.ML	Fri Dec 01 16:08:45 2006 +0100
+++ b/src/HOLCF/domain/theorems.ML	Fri Dec 01 17:22:28 2006 +0100
@@ -213,6 +213,7 @@
       val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
     in Library.foldr mk_ex (vns, conj) end;
 
+  val conj_assoc = thm "conj_assoc";
   val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
   val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
   val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
@@ -350,6 +351,7 @@
 end;
 
 local
+  val rev_contrapos = thm "rev_contrapos";
   fun con_strict (con, args) = 
     let
       fun one_strict vn =
@@ -457,6 +459,7 @@
 end;
 
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
+val rev_contrapos = thm "rev_contrapos";
 
 val distincts_le =
   let