--- a/src/FOL/ex/NatClass.ML Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/NatClass.ML Sat Sep 03 17:15:51 2005 +0200
@@ -5,8 +5,6 @@
This is Nat.ML trivially modified to make it work with NatClass.thy.
*)
-open NatClass;
-
Goal "Suc(k) ~= (k::'a::nat)";
by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);
@@ -54,7 +52,7 @@
by (ALLGOALS (Asm_simp_tac));
qed "add_Suc_right";
-val [prem] = goal NatClass.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
+val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
by (res_inst_tac [("n","i")] induct 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [prem]) 1);