diff -r fb28eaa07e01 -r 3ea049f7979d src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/ex/Qsort.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -24,12 +24,12 @@
 
 Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
 
-goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
+Goal "!x. mset (qsort le xs) x = mset xs x";
 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by (ALLGOALS Asm_simp_tac);
 qed "qsort_permutes";
 
-goal Qsort.thy "set(qsort le xs) = set xs";
+Goal "set(qsort le xs) = set xs";
 by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
 qed "set_qsort";
 Addsimps [set_qsort];
@@ -41,7 +41,7 @@
 qed"Ball_set_filter";
 Addsimps [Ball_set_filter];
 
-goal Qsort.thy
+Goal
  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
 \                     (!x:set xs. !y:set ys. le x y))";
 by (list.induct_tac "xs" 1);
@@ -49,7 +49,7 @@
 qed "sorted_append";
 Addsimps [sorted_append];
 
-goal Qsort.thy 
+Goal 
  "!!le. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
 by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by (ALLGOALS Asm_simp_tac);