avoid ML bindings;

--- a/src/HOL/GroupTheory/Exponent.ML	Tue Aug 28 14:25:26 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML	Wed Aug 29 21:17:24 2001 +0200
@@ -229,14 +229,14 @@
 
 Goal "[|p^k dvd n;  p\\<in>prime;  0<n|] ==> k <= exponent p n";
 by (asm_full_simp_tac (simpset() addsimps [exponent_def]) 1); 
-by (etac Greatest_le 1);
+by (etac (thm "Greatest_le") 1);
 by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 1);  
 qed_spec_mp "exponent_ge";
 
 Goal "0<s ==> (p ^ exponent p s) dvd s";
 by (simp_tac (simpset() addsimps [exponent_def]) 1); 
 by (Clarify_tac 1); 
-by (res_inst_tac [("k","0")] GreatestI 1);
+by (res_inst_tac [("k","0")] (thm "GreatestI") 1);
 by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 2);  
 by (Asm_full_simp_tac 1); 
 qed "power_exponent_dvd";
@@ -251,7 +251,7 @@
 
 Goal "p\\<in>prime ==> exponent p (p^a) = a";
 by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
-by (rtac Greatest_equality 1); 
+by (rtac (thm "Greatest_equality") 1); 
 by (Asm_full_simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1); 
 qed "exponent_power_eq";

--- a/src/HOL/Hilbert_Choice.thy	Tue Aug 28 14:25:26 2001 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 29 21:17:24 2001 +0200
@@ -14,7 +14,7 @@
 
 
 syntax (input)
-  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
+  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
 
 syntax (HOL)
   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
@@ -30,7 +30,7 @@
 
 
 (*used in TFL*)
-lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
+lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
   by (blast intro: someI)
 
 
@@ -59,7 +59,7 @@
 
 lemma LeastMI2:
   "[| P x; !!y. P y ==> m x <= m y;
-           !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]
+           !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
    ==> Q (LeastM m P)";
 apply (unfold LeastM_def)
 apply (rule someI2_ex)
@@ -128,7 +128,7 @@
 lemma GreatestMI2:
      "[| P x;
 	 !!y. P y ==> m y <= m x;
-         !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]
+         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
       ==> Q (GreatestM m P)";
 apply (unfold GreatestM_def)
 apply (rule someI2_ex)
@@ -203,20 +203,6 @@
 done
 
 
-ML {*
-val LeastMI2 = thm "LeastMI2";
-val LeastM_equality = thm "LeastM_equality";
-val GreatestM_def = thm "GreatestM_def";
-val GreatestMI2 = thm "GreatestMI2";
-val GreatestM_equality = thm "GreatestM_equality";
-val Greatest_def = thm "Greatest_def";
-val Greatest_equality = thm "Greatest_equality";
-val GreatestM_natI = thm "GreatestM_natI";
-val GreatestM_nat_le = thm "GreatestM_nat_le";
-val GreatestI = thm "GreatestI";
-val Greatest_le = thm "Greatest_le";
-*}
-
 use "meson_lemmas.ML"
 use "Tools/meson.ML"
 setup meson_setup