diff -r 3a8d722fd3ff -r 16c4ea954511 Subst/AList.ML
--- a/Subst/AList.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Subst/AList.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -34,7 +34,7 @@
 by (etac ssubst 1);
 by (resolve_tac prems 1);
 by (assume_tac 1);
-val alist_induct = result();
+qed "alist_induct";
 
 (*Perform induction on xs. *)
 fun alist_ind_tac a M = 
@@ -46,7 +46,7 @@
     "[| P(Nil);  !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
 by (alist_ind_tac "a" 1);
 by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
-val alist_induct2 = result();
+qed "alist_induct2";
 
 add_inds alist_induct2;
 *)