diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/Message.thy
--- a/src/HOL/MetisExamples/Message.thy	Tue Oct 14 15:45:46 2008 +0200
+++ b/src/HOL/MetisExamples/Message.thy	Tue Oct 14 16:01:36 2008 +0200
@@ -78,7 +78,7 @@
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
-ML{*AtpThread.problem_name := "Message__parts_mono"*}
+ML{*AtpWrapper.problem_name := "Message__parts_mono"*}
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct) 
@@ -102,7 +102,7 @@
 
 subsubsection{*Inverse of keys *}
 
-ML{*AtpThread.problem_name := "Message__invKey_eq"*}
+ML{*AtpWrapper.problem_name := "Message__invKey_eq"*}
 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
 by (metis invKey)
 
@@ -203,7 +203,7 @@
 apply (simp only: parts_Un)
 done
 
-ML{*AtpThread.problem_name := "Message__parts_insert_two"*}
+ML{*AtpWrapper.problem_name := "Message__parts_insert_two"*}
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
@@ -240,7 +240,7 @@
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
-ML{*AtpThread.problem_name := "Message__parts_subset_iff"*}
+ML{*AtpWrapper.problem_name := "Message__parts_subset_iff"*}
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 apply (rule iffI) 
 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
@@ -251,7 +251,7 @@
 by (blast dest: parts_mono); 
 
 
-ML{*AtpThread.problem_name := "Message__parts_cut"*}
+ML{*AtpWrapper.problem_name := "Message__parts_cut"*}
 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
 by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
 
@@ -316,7 +316,7 @@
 done
 
 
-ML{*AtpThread.problem_name := "Message__msg_Nonce_supply"*}
+ML{*AtpWrapper.problem_name := "Message__msg_Nonce_supply"*}
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
 apply (induct_tac "msg") 
 apply (simp_all add: parts_insert2)
@@ -368,7 +368,7 @@
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
 
 
-ML{*AtpThread.problem_name := "Message__parts_analz"*}
+ML{*AtpWrapper.problem_name := "Message__parts_analz"*}
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (metis analz_subset_parts parts_subset_iff)
@@ -520,7 +520,7 @@
 by (drule analz_mono, blast)
 
 
-ML{*AtpThread.problem_name := "Message__analz_cut"*}
+ML{*AtpWrapper.problem_name := "Message__analz_cut"*}
     declare analz_trans[intro]
 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
 (*TOO SLOW
@@ -538,7 +538,7 @@
 
 text{*A congruence rule for "analz" *}
 
-ML{*AtpThread.problem_name := "Message__analz_subset_cong"*}
+ML{*AtpWrapper.problem_name := "Message__analz_subset_cong"*}
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
@@ -616,7 +616,7 @@
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 
-ML{*AtpThread.problem_name := "Message__synth_insert"*}
+ML{*AtpWrapper.problem_name := "Message__synth_insert"*}
  
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
@@ -638,7 +638,7 @@
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
 
-ML{*AtpThread.problem_name := "Message__synth_cut"*}
+ML{*AtpWrapper.problem_name := "Message__synth_cut"*}
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 (*TOO SLOW
 by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
@@ -670,7 +670,7 @@
 
 subsubsection{*Combinations of parts, analz and synth *}
 
-ML{*AtpThread.problem_name := "Message__parts_synth"*}
+ML{*AtpWrapper.problem_name := "Message__parts_synth"*}
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
@@ -685,14 +685,14 @@
 
 
 
-ML{*AtpThread.problem_name := "Message__analz_analz_Un"*}
+ML{*AtpWrapper.problem_name := "Message__analz_analz_Un"*}
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (rule equalityI);
 apply (metis analz_idem analz_subset_cong order_eq_refl)
 apply (metis analz_increasing analz_subset_cong order_eq_refl)
 done
 
-ML{*AtpThread.problem_name := "Message__analz_synth_Un"*}
+ML{*AtpWrapper.problem_name := "Message__analz_synth_Un"*}
     declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 apply (rule equalityI)
@@ -706,7 +706,7 @@
 done
 
 
-ML{*AtpThread.problem_name := "Message__analz_synth"*}
+ML{*AtpWrapper.problem_name := "Message__analz_synth"*}
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 proof (neg_clausify)
 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
@@ -729,7 +729,7 @@
 
 subsubsection{*For reasoning about the Fake rule in traces *}
 
-ML{*AtpThread.problem_name := "Message__parts_insert_subset_Un"*}
+ML{*AtpWrapper.problem_name := "Message__parts_insert_subset_Un"*}
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
 proof (neg_clausify)
 assume 0: "X \<in> G"
@@ -748,7 +748,7 @@
   by (metis 6 0)
 qed
 
-ML{*AtpThread.problem_name := "Message__Fake_parts_insert"*}
+ML{*AtpWrapper.problem_name := "Message__Fake_parts_insert"*}
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
@@ -791,14 +791,14 @@
       ==> Z \<in>  synth (analz H) \<union> parts H";
 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
 
-ML{*AtpThread.problem_name := "Message__Fake_analz_insert"*}
+ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert"*}
     declare analz_mono [intro] synth_mono [intro] 
 lemma Fake_analz_insert:
      "X\<in> synth (analz G) ==>  
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
 
-ML{*AtpThread.problem_name := "Message__Fake_analz_insert_simpler"*}
+ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert_simpler"*}
 (*simpler problems?  BUT METIS CAN'T PROVE
 lemma Fake_analz_insert_simpler:
      "X\<in> synth (analz G) ==>