diff -r fb28eaa07e01 -r 3ea049f7979d src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -21,23 +21,23 @@
 
 (*** Congruence rules for ->> ***)
 
-goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
+Goal "!!s. s ->> s' ==> Abs s ->> Abs s'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_Abs";
 AddSIs [rtrancl_beta_Abs];
 
-goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
+Goal "!!s. s ->> s' ==> s @ t ->> s' @ t";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppL";
 
-goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
+Goal "!!s. t ->> t' ==> s @ t ->> s @ t'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppR";
 
-goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
+Goal "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
 by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
                        addIs  [rtrancl_trans]) 1);
 qed "rtrancl_beta_App";
@@ -49,22 +49,22 @@
                      delsplits [split_if]
                      setloop (split_inside_tac [split_if]);
 
-goal Lambda.thy "(Var k)[u/k] = u";
+Goal "(Var k)[u/k] = u";
 by (asm_full_simp_tac(addsplit(simpset())) 1);
 qed "subst_eq";
 
-goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(j-1)";
+Goal "!!s. i<j ==> (Var j)[u/i] = Var(j-1)";
 by (asm_full_simp_tac(addsplit(simpset())) 1);
 qed "subst_gt";
 
-goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)";
+Goal "!!s. j<i ==> (Var j)[u/i] = Var(j)";
 by (asm_full_simp_tac (addsplit(simpset()) addsimps
                           [less_not_refl2 RS not_sym,less_SucI]) 1);
 qed "subst_lt";
 
 Addsimps [subst_eq,subst_gt,subst_lt];
 
-goal Lambda.thy
+Goal
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
@@ -72,7 +72,7 @@
 by (ALLGOALS trans_tac);
 qed_spec_mp "lift_lift";
 
-goal Lambda.thy "!i j s. j < Suc i --> \
+Goal "!i j s. j < Suc i --> \
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
@@ -83,7 +83,7 @@
 qed "lift_subst";
 Addsimps [lift_subst];
 
-goal Lambda.thy
+Goal
   "!i j s. i < Suc j -->\
 \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
 by (dB.induct_tac "t" 1);
@@ -93,14 +93,14 @@
 by (ALLGOALS trans_tac);
 qed "lift_subst_lt";
 
-goal Lambda.thy "!k s. (lift t k)[s/k] = t";
+Goal "!k s. (lift t k)[s/k] = t";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_lift";
 Addsimps [subst_lift];
 
 
-goal Lambda.thy "!i j u v. i < Suc j --> \
+Goal "!i j u v. i < Suc j --> \
 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
@@ -116,25 +116,25 @@
 
 (*** Equivalence proof for optimized substitution ***)
 
-goal Lambda.thy "!k. liftn 0 t k = t";
+Goal "!k. liftn 0 t k = t";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
 qed "liftn_0";
 Addsimps [liftn_0];
 
-goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
+Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
 by (blast_tac (claset() addDs [add_lessD1]) 1);
 qed "liftn_lift";
 Addsimps [liftn_lift];
 
-goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
+Goal "!n. substn t s n = t[liftn n s 0 / n]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
 qed "substn_subst_n";
 Addsimps [substn_subst_n];
 
-goal Lambda.thy "substn t s 0 = t[s/0]";
+Goal "substn t s 0 = t[s/0]";
 by (Simp_tac 1);
 qed "substn_subst_0";