--- 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));