diff -r fb28eaa07e01 -r 3ea049f7979d src/HOL/Map.ML
--- a/src/HOL/Map.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Map.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -6,12 +6,12 @@
 Map lemmas
 *)
 
-goalw thy [empty_def] "empty k = None";
+Goalw [empty_def] "empty k = None";
 by (Simp_tac 1);
 qed "empty_def2";
 Addsimps [empty_def2];
 
-goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
+Goalw [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
 by (Simp_tac 1);
 qed "update_def2";
 Addsimps [update_def2];
@@ -36,12 +36,12 @@
 
 section "++";
 
-goalw thy [override_def] "m ++ empty = m";
+Goalw [override_def] "m ++ empty = m";
 by (Simp_tac 1);
 qed "override_empty";
 Addsimps [override_empty];
 
-goalw thy [override_def] "empty ++ m = m";
+Goalw [override_def] "empty ++ m = m";
 by (Simp_tac 1);
 by (rtac ext 1);
 by (split_tac [split_option_case] 1);
@@ -49,20 +49,20 @@
 qed "empty_override";
 Addsimps [empty_override];
 
-goalw thy [override_def]
+Goalw [override_def]
  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
 by (simp_tac (simpset() addsplits [split_option_case]) 1);
 qed_spec_mp "override_Some_iff";
 
 bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
 
-goalw thy [override_def]
+Goalw [override_def]
  "((m ++ n) k = None) = (n k = None & m k = None)";
 by (simp_tac (simpset() addsplits [split_option_case]) 1);
 qed "override_None";
 AddIffs [override_None];
 
-goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
+Goalw [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
 by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (rtac ext 1);
@@ -70,7 +70,7 @@
 qed "map_of_append";
 Addsimps [map_of_append];
 
-goal thy "map_of xs k = Some y --> (k,y):set xs";
+Goal "map_of xs k = Some y --> (k,y):set xs";
 by (list.induct_tac "xs" 1);
 by  (Simp_tac 1);
 by (split_all_tac 1);
@@ -79,12 +79,12 @@
 
 section "dom";
 
-goalw thy [dom_def] "dom empty = {}";
+Goalw [dom_def] "dom empty = {}";
 by (Simp_tac 1);
 qed "dom_empty";
 Addsimps [dom_empty];
 
-goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
+Goalw [dom_def] "dom(m[a|->b]) = insert a (dom m)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "dom_update";
@@ -96,19 +96,19 @@
 	stac (insert_Collect RS sym) 1,
 	Asm_simp_tac 1]);
 
-goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
+Goalw [dom_def] "dom(m++n) = dom n Un dom m";
 by (Blast_tac 1);
 qed "dom_override";
 Addsimps [dom_override];
 
 section "ran";
 
-goalw thy [ran_def] "ran empty = {}";
+Goalw [ran_def] "ran empty = {}";
 by (Simp_tac 1);
 qed "ran_empty";
 Addsimps [ran_empty];
 
-goalw thy [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)";
+Goalw [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)";
 by Auto_tac;
 by (subgoal_tac "~(aa = a)" 1);
 by Auto_tac;