diff -r 978854c19b5e -r 9e33eddca122 ex/Term.ML
--- a/ex/Term.ML	Fri Nov 25 09:12:16 1994 +0100
+++ b/ex/Term.ML	Fri Nov 25 09:59:51 1994 +0100
@@ -44,7 +44,7 @@
 by (REPEAT (eresolve_tac ([minor] @
  		([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
 (*Proof could also use  mono_Int RS subsetD RS IntE *)
-val term_induct = result();
+qed "Term_induct";
 
 (*Induction on term(A) followed by induction on list *)
 val major::prems = goal Term.thy
@@ -53,10 +53,10 @@
 \       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
 \                 |] ==> R(x $ CONS(z,zs))  \
 \    |] ==> R(M)";
-by (rtac (major RS term_induct) 1);
+by (rtac (major RS Term_induct) 1);
 by (etac list.induct 1);
 by (REPEAT (ares_tac prems 1));
-qed "term_induct2";
+qed "Term_induct2";
 
 (*** Structural Induction on the abstract type 'a term ***)
 
@@ -71,7 +71,7 @@
 \    |] ==> R(t)";
 by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
 by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
-by (rtac (Rep_term RS term_induct) 1);
+by (rtac (Rep_term RS Term_induct) 1);
 by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
     list_subset_sexp, range_Leaf_subset_sexp] 1
      ORELSE etac rev_subsetD 1));