# HG changeset patch
# User paulson
# Date 861702322 -7200
# Node ID 0a887d5b6718d00415c84182ab25a85d38e07ee1
# Parent  e5efa177ee0c64770bb182177c2e2454bee3c400
Ran expandshort

diff -r e5efa177ee0c -r 0a887d5b6718 src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Tue Apr 22 11:45:22 1997 +0200
@@ -74,8 +74,8 @@
 \                       else TVar x) o \
 \                  (%x. if x : free_tv A \
 \                       then x else n + x)) A)";
-by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1);
-by (rtac (alpha_A RS ssubst) 1);
+by (stac S_o_alpha_type_scheme_list 1);
+by (stac alpha_A 1);
 by (rtac refl 1);
 qed "S'_A_eq_S'_alpha_A";
 
diff -r e5efa177ee0c -r 0a887d5b6718 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/MiniML/Type.ML	Tue Apr 22 11:45:22 1997 +0200
@@ -318,9 +318,9 @@
      "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
 \     free_tv s1 Un free_tv s2";
 by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
-			     free_tv_subst_var RS subsetD] 
-	             addss (!simpset delsimps bex_simps
-				     addsimps [cod_def,dom_def])) 1);
+                             free_tv_subst_var RS subsetD] 
+                     addss (!simpset delsimps bex_simps
+                                     addsimps [cod_def,dom_def])) 1);
 qed "free_tv_comp_subst";
 
 goalw thy [o_def] 
@@ -481,7 +481,7 @@
 goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS (Asm_full_simp_tac));
-by (rewrite_goals_tac [new_tv_def]);
+by (rewtac new_tv_def);
 by (simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
 by (strip_tac 1);
 by (case_tac "S nat = TVar nat" 1);
@@ -638,7 +638,7 @@
 by (REPEAT (etac exE 1));
 by (rename_tac "n2 n1" 1);
 by (res_inst_tac [("x","(max n1 n2)")] exI 1);
-by (rewrite_goals_tac [new_tv_def]);
+by (rewtac new_tv_def);
 by (fast_tac (!claset addIs [less_maxL,less_maxR]) 1);
 qed "ex_fresh_variable";
 
diff -r e5efa177ee0c -r 0a887d5b6718 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/MiniML/W.ML	Tue Apr 22 11:45:22 1997 +0200
@@ -206,13 +206,13 @@
 ba 1;
 ba 1;
 ba 1;
-by (rewrite_goals_tac [new_tv_def]);
+by (rewtac new_tv_def);
 by (Asm_simp_tac 1);
 by (dtac W_var_ge 1);
 by (rtac allI 1);
 by (rename_tac "p" 1);
 by (strip_tac 1);
-by (rewrite_goals_tac [free_tv_subst]);
+by (rewtac free_tv_subst);
 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
 fun restrict_prems is tacf =
   METAHYPS(fn prems =>
@@ -494,7 +494,7 @@
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
                   unsafe_addss (!simpset addcongs [conj_cong] 
-				setloop (split_tac [expand_option_bind]))) 1);
+                                setloop (split_tac [expand_option_bind]))) 1);
 (** LEVEL 19 **)
 
 (* case App e1 e2 *)
diff -r e5efa177ee0c -r 0a887d5b6718 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Tue Apr 22 11:37:12 1997 +0200
+++ b/src/HOL/W0/W.ML	Tue Apr 22 11:45:22 1997 +0200
@@ -174,7 +174,7 @@
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (fast_tac (HOL_cs addSEs [allE]
-	             addIs [cod_app_subst]
+                     addIs [cod_app_subst]
                      addss (!simpset addsimps [less_Suc_eq])) 1);
 (** LEVEL 12 **)
 (* case App e1 e2 *)
@@ -211,11 +211,11 @@
 by (dtac (sym RS W_var_geD) 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
-			    free_tv_app_subst_te RS subsetD,
-			    free_tv_app_subst_tel RS subsetD,
-			    less_le_trans,subsetD]
-	             addSEs [UnE]
-		     addss !simpset) 1); 
+                            free_tv_app_subst_te RS subsetD,
+                            free_tv_app_subst_tel RS subsetD,
+                            less_le_trans,subsetD]
+                     addSEs [UnE]
+                     addss !simpset) 1); 
 qed_spec_mp "free_tv_W"; 
 
 (* Completeness of W w.r.t. has_type *)
@@ -370,7 +370,7 @@
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
-			    eq_subst_tel_eq_free] 
+                            eq_subst_tel_eq_free] 
        addss ((!simpset addsimps [free_tv_subst,dom_def]))) 1);
 (** LEVEL 106 **)
 by (Fast_tac 1);